Readings shared July 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/22-readings_shared_07-21-25 #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #Rocq

Readings shared July 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/22-readings_shared_07-21-25 #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #Rocq
Representability and formalization of (distributive quasi) relation algebras. ~ Peter Jipsen. https://iphils.uj.edu.pl/clock/2025/slides/jipsen.pdf #ITP #LeanProver #IsabelleHOL #Rocq #Math
Scaling mathematical reasoning through data, tools, and generative selection. ~ Ivan Moshkov et als. https://openreview.net/forum?id=OM7ZN0PmSS #LLMs #ITP #LeanProver #Math
Readings shared July 18, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/19-readings_shared_07-18-25 #ACL2 #CompSci #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Rocq #Rust #Teaching
Leanabell-Prover-V2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. ~ Xingguang Ji et als. https://arxiv.org/abs/2507.08649v1 #LLMs #ITP #LeanProver
CSLib: An open-source Lean 4 library formalizing a significant subsetof undergraduate-level computer science. ~ Clark Barrett et als. https://docs.google.com/presentation/d/1aJFM3EaI4LcppHR_2YFQHiBjUfMMhMKxCeM3BfINi48 #ITP #LeanProver #CompSci
Bourbaki: Self-generated and goal-conditioned MDPs for theorem proving. ~ Matthieu Zimmer et als. https://arxiv.org/abs/2507.02726v1 #LLMs #ITP #LeanProver
The φ-weighted recognition hamiltonian: A self-adjoint operator unifying automorphic L-functions, E 8 symmetry, and cosmic dynamics. https://www.researchgate.net/publication/393400892_The_ph-Weighted_Recognition_Hamiltonian_A_Self-Adjoint_Operator_Unifying_Automorphic_L-Functions_E_8_Symmetry_and_Cosmic_Dynamics #ITP #LeanProver
Doing Lean dirty: Lean as a Jupyter notebook replacement. ~ Philip Zucker. https://www.philipzucker.com/dirty_lean/ #ITP #LeanProver
Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. https://arxiv.org/abs/2405.19270 #ITP #LeanProver #Math
Readings shared July 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/08-readings_shared_07-07-25 #Coq #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Maxima
We're excited to share the new lean-lang.org!
Relaunching our website was a key deliverable in our Year 2 roadmap to provide "improved navigation and access to valuable content, resources, and tools." We hope you like it!
Lean: a theorem prover and programming language that enables correct, maintainable, and formally verified code. https://lean-lang.org #ITP #LeanProver #FunctionalProgramming
The filter game (in Lean 4). ~ Kevin Buzzard. https://adam.math.hhu.de/#/g/kbuzzard/FilterGame #ITP #LeanProver #Math
Functorial flattening of the state monad via vector‐space projection (A formally verified collapse model in Lean 4). ~ Jinu Jang. https://kairose-master.github.io/mu_eq_pi/pdf/mu_eq_pi.pdf #ITP #LeanProver
Reseña de «LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving». https://jaalonso.github.io/vestigium/posts/2025/07/04-leanconjecturer-automatic-generation-of-mathematical-conjectures-for-theorem-proving/ #ITP #LeanProver #Math #LLMs
LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving. ~ Naoto Onda et als. https://arxiv.org/abs/2506.22005v1 #ITP #LeanProver #Math #LLMs
Readings shared July 3, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/04-readings_shared_07-03-25 #ITP #LeanProver #Agda