LeanProver

Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ⊆ u s ⊆ f⁻¹(u)". https://jaalonso.github.io/calculemus/posts/2021/06/08-subconjunto_de_la_imagen_inversa/ #LeanProver #IsabelleHOL #Math #Calculemus

Arithmetic progressions - almost periodicity (A digitisation of the Kelley-Meka bound on Roth numbers in Lean). ~ Thomas Bloom, Yaël Dillies. https://yaeldillies.github.io/LeanAPAP/ #ITP #LeanProver #Math

Toric varieties in Lean (Formalisation of toric varieties in Lean 4). ~ Yaël Dillies, Paul Lezeau, Patrick Luo, Michał Mrugała, Justus Springer, Andrew Yang. https://yaeldillies.github.io/Toric/ #ITP #LeanProver #Math

Chandra-Furst-Lipton (A digitisation of the number on the forehead model in Lean). ~ Yaël Dillies. https://yaeldillies.github.io/ChandraFurstLipton/ #ITP #LeanProver #Math

Learn Lean 4 with PLFA (Programming Language Foundations in Agda) proofs. ~ rami3l. https://github.com/rami3l/plfl #ITP #LeanProver

Formalizing value distribution theory in Lean. ~ Stefan Kebekus. https://github.com/kebekus/ProjectVD #ITP #LeanProver #Math

Prime number theorem and more in Lean. ~ Alex Kontorovich. https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/ #ITP #LeanProver #Math

Central limit theorem in Lean. ~ Rémy Degenne. https://remydegenne.github.io/CLT/blueprint #ITP #LeanProver #Math

Lecture notes for an introductory course in group theory. ~ Ben Selfridge. https://github.com/benjaminselfridge/group-theory-course/tree/main #ITP #LeanProver #Math

Readings shared April 6, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/06-readings_shared_04-06-25 #AI #Haskell #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #ProgramaciónFuncional #Prolog

Demostraciones con Lean4 y con Isabelle/HOL de "s ⊆ f⁻¹(f(s))". https://jaalonso.github.io/calculemus/posts/2021/06/07-imagen_inversa_de_la_imagen/ #LeanProver #IsabelleHOL #Math #Calculemus

Readings shared April 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/05-readings_shared_04-05-25 #FunctionalProgramming #Haskell #IsabelleHOL #LeanProver #Logic #LogicProgramming #Math #Prolog

Demostraciones con Lean4 y con Isabelle/HOL de "f(s ∪ t) = f(s) ∪ f(t)". https://jaalonso.github.io/calculemus/posts/2021/06/06-imagen_de_la_union/ #LeanProver #IsabelleHOL #Math #Calculemus

Readings shared April 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/04-readings_shared_04-04-25 #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Maxima

Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)". https://jaalonso.github.io/calculemus/posts/2021/06/05-imagen_inversa_de_la_interseccion/ #LeanProver #IsabelleHOL #Math #Calculemus

Learning Lean in the age of Artificial Intelligence. ~ Adolfo Neto. https://youtu.be/plpPffJOKu8 #ITP #LeanProver

Readings shared April 3, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/03-readings_shared_04-03-25 #AI #AlphaProof #CategoryTheory #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math

Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)". https://jaalonso.github.io/calculemus/posts/2021/06/04-union_con_interseccion_general/ #LeanProver #IsabelleHOL #Math #Calculemus

LeanSolver: Solving theorems through large language models and search. ~ Avi Luciano Halevy https://repository.tudelft.nl/file/File_a98b6c93-4017-42c5-bb8f-df68da0d7034 #LLMs #ITP #LeanProver

Readings shared April 2, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/02-readings_shared_04-02-25 #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Mathlib #Prolog