Human skepticism and formal verification. ~ Benjamin Friedman.
https://proofsandprompts.com/2026/11/13/human-skepticism-and-formal-verification/
#leanlang — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #leanlang, aggregated by home.social.
-
Statopia: A prover-library ecosystem for automated formalization and proof discovery in statistics. ~ Ziyuan Chen, Tong Gan, Wei Zhang, Ruofei Fang, Boyue Tang, Zhenhua Lin, Fang Yao.
-
No regular icosahedron has a rational point on every face: a proof checked in Lean. ~ Mikhail Levit.
-
Braid groups in Lean : Formalizing Dehornoy's subword reversing algorithm. ~ Hannah Fechtner.
-
No regular icosahedron has a rational point on every face: a proof checked in Lean. ~ Mikhail Levit.
-
Formal proof of an anisotropic Calderón uniqueness theorem. ~ Cătălin I. Cârstea, Lauri Oksanen.
-
Lean 4 challenge 25: If the interleaving of two sequences converges to L, then both converge to L.
https://jaalonso.github.io/calculemus/en/posts/2026/10/26-convergencia_de_la_mezcla_de_sucesiones/
-
Reto 25 de Lean 4: Si la mezcla de dos sucesiones converge a L, entonces ambas convergen a L.
https://jaalonso.github.io/calculemus/posts/2026/10/26-convergencia_de_la_mezcla_de_sucesiones/
-
Lean Grimoire: a proof-crafting game. ~ Terence Tao.
-
Lean Grimoire. ~ Terence Tao.
-
"…and the proof is checked in Lean". ~ Kevin Buzzard.
https://xenaproject.wordpress.com/2026/11/12/and-the-proof-is-checked-in-lean/
-
Leab 4 Challenge 24: The sequence 1, -1, 1, -1,... is not convergent (2nd version).
https://jaalonso.github.io/calculemus/en/posts/2026/10/19-no_convergencia_-1n_v2/
-
Reto 24 de Lean 4: La sucesión 1, -1, 1, -1,... no es convergente (2ª versión).
https://jaalonso.github.io/calculemus/posts/2026/10/19-no_convergencia_-1n_v2/