#leanprover — Public Fediverse posts

AnnalsChallenge is a collection of formalised statements of recent important theorems. These theorems are the main results of papers published in the Annals of Mathematics in the 2020s. The statements are written in Lean 4, using Mathlib. https://github.com/ImperialCollegeLondon/AnnalsChallenge #LeanProver #ITP #Math

AnnalsChallenge is a collection of formalised statements of recent important theorems. These theorems are the main results of papers published in the Annals of Mathematics in the 2020s. The statements are written in Lean 4, using Mathlib. https://github.com/ImperialCollegeLondon/AnnalsChallenge #LeanProver #ITP #Math

The Annals Challenge. ~ Kevin Buzzard. https://xenaproject.wordpress.com/2026/08/13/the-annals-challenge/ #LeanProver #ITP #Math

The Annals Challenge. ~ Kevin Buzzard. https://xenaproject.wordpress.com/2026/08/13/the-annals-challenge/ #LeanProver #ITP #Math

The Lean Kernel Arena presents, tests and benchmarks proof checkers for the Lean Theorem Prover. https://arena.lean-lang.org/ #LeanProver #ITP

The Lean Kernel Arena presents, tests and benchmarks proof checkers for the Lean Theorem Prover. https://arena.lean-lang.org/ #LeanProver #ITP

Vero: Can AI agents build formally verified software repositories? ~ Zhe Ye et als. https://arxiv.org/abs/2608.13522 #LeanProver #ITP #FormalVerification

Vero: Can AI agents build formally verified software repositories? ~ Zhe Ye et als. https://arxiv.org/abs/2608.13522 #LeanProver #ITP #FormalVerification

The Gaussian code bridge: E8 over Z[i], the extended Hamming code, and a four-bit information layer. ~ Stefan Hamann. https://www.fixpoint-theory.com/papers/note_e8_gaussian_code.pdf #LeanProver #ITP

The Gaussian code bridge: E8 over Z[i], the extended Hamming code, and a four-bit information layer. ~ Stefan Hamann. https://www.fixpoint-theory.com/papers/note_e8_gaussian_code.pdf #LeanProver #ITP

Banach lattices and phase retrieval: A case study for the use of AI in mathematics. ~ Jaume de Dios Pont, Lukas Liehr, David Muñoz-Lahoz, Mitchell A. Taylor, Pedro Tradacete. https://arxiv.org/abs/2608.07396v1 #LeanProver #ITP #AI4Math

Banach lattices and phase retrieval: A case study for the use of AI in mathematics. ~ Jaume de Dios Pont, Lukas Liehr, David Muñoz-Lahoz, Mitchell A. Taylor, Pedro Tradacete. https://arxiv.org/abs/2608.07396v1 #LeanProver #ITP #AI4Math

The Banach lattice Lean library. ~ David Muñoz-Lahoz. https://arxiv.org/abs/2608.07388v1 #LeanProver #ITP #Math

The Banach lattice Lean library. ~ David Muñoz-Lahoz. https://arxiv.org/abs/2608.07388v1 #LeanProver #ITP #Math

The set of primes is supernatural: a Lean formalization of the statement of the conjecture. ~ A. Mayeux. https://arxiv.org/abs/2608.08643v1 #LeanProver #ITP #Math

The set of primes is supernatural: a Lean formalization of the statement of the conjecture. ~ A. Mayeux. https://arxiv.org/abs/2608.08643v1 #LeanProver #ITP #Math

Dilatations of categories, via their lean formalization. ~ Arnaud Mayeux. https://arxiv.org/abs/2608.09305v1 #LeanProver #ITP

Dilatations of categories, via their lean formalization. ~ Arnaud Mayeux. https://arxiv.org/abs/2608.09305v1 #LeanProver #ITP

Deep Vision: A formal proof of Wolstenholmes theorem in Lean 4. ~ Alexandre Linhares. https://arxiv.org/abs/2604.16507v2 #LeanProver #ITP #AI4Math

Deep Vision: A formal proof of Wolstenholmes theorem in Lean 4. ~ Alexandre Linhares. https://arxiv.org/abs/2604.16507v2 #LeanProver #ITP #AI4Math

A proof of the Dittert conjecture in dimension 4 via an exact constrained sum-of-squares certificate. ~ Jinhui Li, Beibei Xiong, Zhengfeng Yang. https://arxiv.org/abs/2607.29191v2 #LeanProver #ITP #Math

A proof of the Dittert conjecture in dimension 4 via an exact constrained sum-of-squares certificate. ~ Jinhui Li, Beibei Xiong, Zhengfeng Yang. https://arxiv.org/abs/2607.29191v2 #LeanProver #ITP #Math

Lean 4.33.0 is live! https://lean-lang.org/doc/reference/latest/releases/v4.33.0/ #LeanProver #ITP

Lean 4.33.0 is live! https://lean-lang.org/doc/reference/latest/releases/v4.33.0/ #LeanProver #ITP

TheoremDB: A public workspace for machine mathematics. https://theoremdb.org/ #AI4Math #LeanProver

TheoremDB: A public workspace for machine mathematics. https://theoremdb.org/ #AI4Math #LeanProver

𝐋𝐞𝐚𝐧 𝟒.𝟑𝟑.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings 208 changes, including a more responsive editor, automatic proof suggestions, and 𝙵𝚕𝚘𝚊𝚝 no longer being an opaque type. Notable improvements include:

⚡ Editing feels smoother: the editor now preserves your progress when you press return after a tactic, and proof-search tactics respond faster near the top of long files

✨ 𝚝𝚛𝚢? can now suggest proofs automatically at empty proofs, unsolved goals, or 𝚜𝚘𝚛𝚛𝚢, with no change needed to how proofs are written

🧠 The 𝚕𝚒𝚊 and 𝚐𝚛𝚒𝚗𝚍 tactics can now close more goals automatically, including ones involving 𝚖𝚒𝚗/𝚖𝚊𝚡 and bitvector arithmetic

🔧 𝙵𝚕𝚘𝚊𝚝 numbers now have a logical model behind them, letting downstream libraries build and verify their own theorems about floating-point behavior

𝐅𝐮𝐥𝐥 𝐫𝐞𝐥𝐞𝐚𝐬𝐞 𝐧𝐨𝐭𝐞𝐬: https://lean-lang.org/doc/reference/latest/releases/v4.33.0/

#LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification

𝐋𝐞𝐚𝐧 𝟒.𝟑𝟑.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings 208 changes, including a more responsive editor, automatic proof suggestions, and 𝙵𝚕𝚘𝚊𝚝 no longer being an opaque type. Notable improvements include:

⚡ Editing feels smoother: the editor now preserves your progress when you press return after a tactic, and proof-search tactics respond faster near the top of long files

✨ 𝚝𝚛𝚢? can now suggest proofs automatically at empty proofs, unsolved goals, or 𝚜𝚘𝚛𝚛𝚢, with no change needed to how proofs are written

🧠 The 𝚕𝚒𝚊 and 𝚐𝚛𝚒𝚗𝚍 tactics can now close more goals automatically, including ones involving 𝚖𝚒𝚗/𝚖𝚊𝚡 and bitvector arithmetic

🔧 𝙵𝚕𝚘𝚊𝚝 numbers now have a logical model behind them, letting downstream libraries build and verify their own theorems about floating-point behavior

𝐅𝐮𝐥𝐥 𝐫𝐞𝐥𝐞𝐚𝐬𝐞 𝐧𝐨𝐭𝐞𝐬: https://lean-lang.org/doc/reference/latest/releases/v4.33.0/

#LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification

Interesting viewpoint on #leanprover and encoding pure math in type theory that @tobsboe just pointed me to:

https://mathoverflow.net/questions/513540/should-we-trust-ai-generated-formal-proofs-in-lean-4/513585#513585

In-type junk values are another extremely efficient footgun when working with proof assistants.

Interesting viewpoint on #leanprover and encoding pure math in type theory that @tobsboe just pointed me to:

https://mathoverflow.net/questions/513540/should-we-trust-ai-generated-formal-proofs-in-lean-4/513585#513585

In-type junk values are another extremely efficient footgun when working with proof assistants.

From the Dirichlet integral to Lobachevsky's formula: a formalization in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07366v1 #LeanProver #ITP #Math

From the Dirichlet integral to Lobachevsky's formula: a formalization in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07366v1 #LeanProver #ITP #Math

A formalization of the Laplace transform and its inversion in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07384 #LeanProver #ITP #Math

A formalization of the Laplace transform and its inversion in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. https://arxiv.org/abs/2608.07384 #LeanProver #ITP #Math

Readings shared: 3 – 9 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/10-readings_shared_08-10-26 #AI #AI4Math #Coq #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math

Readings shared: 3 – 9 August, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/10-readings_shared_08-10-26 #AI #AI4Math #Coq #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math

#RetoLean4: Enunciado del reto 14 (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). https://t.me/Retos_Matematicos/109557/142663 #LeanProver #ITP #Math

#RetoLean4: Enunciado del reto 14 (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). https://t.me/Retos_Matematicos/109557/142663 #LeanProver #ITP #Math

#Retolean4: Vídeo tutorial sobre cómo resolver el reto 13. https://youtu.be/EcNgDxgNya8 #LeanProver #ITP #Math

#Retolean4: Vídeo tutorial sobre cómo resolver el reto 13. https://youtu.be/EcNgDxgNya8 #LeanProver #ITP #Math

#RetoLean4: Soluciones del reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). https://live.lean-lang.org/#url=https://github.com/jaalonso/Retos/blob/main/src/Reto_13.lean #LeanProver #ITP #Math

#RetoLean4: Soluciones del reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). https://live.lean-lang.org/#url=https://github.com/jaalonso/Retos/blob/main/src/Reto_13.lean #LeanProver #ITP #Math

Game hopping in Lean. ~ Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał Stefański. https://arxiv.org/abs/2608.06261 #LeanProver #ITP

Game hopping in Lean. ~ Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał Stefański. https://arxiv.org/abs/2608.06261 #LeanProver #ITP

A formalization of the mean-field derivation of the Vlasov equation (Mathematician in the loop: AI-assisted Lean formalization as a strategy game). ~ Joseph K. Miller. https://arxiv.org/abs/2607.08986v2 #LeanProver #ITP #AI4Math

A formalization of the mean-field derivation of the Vlasov equation (Mathematician in the loop: AI-assisted Lean formalization as a strategy game). ~ Joseph K. Miller. https://arxiv.org/abs/2607.08986v2 #LeanProver #ITP #AI4Math

Topological semantics for scoped computational paths. ~ Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras. https://arxiv.org/abs/2608.04228v1 #LeanProver #ITP #Math

Topological semantics for scoped computational paths. ~ Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras. https://arxiv.org/abs/2608.04228v1 #LeanProver #ITP #Math

Every quasiperfect number has at least eight distinct prime factors. ~ Akira Toyohara, Ye Tao, Siqiong Yao. https://arxiv.org/abs/2608.02066v1 #LeanProver #ITP #AI4Math

Every quasiperfect number has at least eight distinct prime factors. ~ Akira Toyohara, Ye Tao, Siqiong Yao. https://arxiv.org/abs/2608.02066v1 #LeanProver #ITP #AI4Math

Verifying Verus: A Lean 4 formalization of the SST-to-AIR expression translation. ~ Shuge Rong. https://www.andrew.cmu.edu/user/avigad/Students/rong_ms_thesis.pdf #LeanProver #ITP

Verifying Verus: A Lean 4 formalization of the SST-to-AIR expression translation. ~ Shuge Rong. https://www.andrew.cmu.edu/user/avigad/Students/rong_ms_thesis.pdf #LeanProver #ITP

Fitting’s theorem and semirings of normal subgroups. ~ Damiano Testa. https://arxiv.org/abs/2607.29111v1 #LeanProver #ITP #AI4Math

Fitting’s theorem and semirings of normal subgroups. ~ Damiano Testa. https://arxiv.org/abs/2607.29111v1 #LeanProver #ITP #AI4Math

A bijective proof of a partition theorem of Berkovich and Uncu. ~ Michal Mogielnicki, Ken Ono, Niels Voss, Jujian Zhang. https://arxiv.org/abs/2608.05142v1 #AI4Math #LeanProver #ITP

A bijective proof of a partition theorem of Berkovich and Uncu. ~ Michal Mogielnicki, Ken Ono, Niels Voss, Jujian Zhang. https://arxiv.org/abs/2608.05142v1 #AI4Math #LeanProver #ITP

PutnamBench Leaderboard (Benchmarking formal mathematical reasoning on the Putnam Mathematical Competition). https://trishullab.github.io/PutnamBench/leaderboard #AI4Math #LeanProver #IsabelleHOL #Coq

PutnamBench Leaderboard (Benchmarking formal mathematical reasoning on the Putnam Mathematical Competition). https://trishullab.github.io/PutnamBench/leaderboard #AI4Math #LeanProver #IsabelleHOL #Coq

Lean4Lean: Verifying a typechecker for Lean, in Lean. ~ Mario Carneiro. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.2 #LeanProver #ITP

Lean4Lean: Verifying a typechecker for Lean, in Lean. ~ Mario Carneiro. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.2 #LeanProver #ITP