Readings shared April 7, 2025
- Verified program extraction in number theory: The fundamental theorem of arithmetic and relatives. ~ Franziskus Wiesnet. #ITP #Minlog #Haskell #FunctionalProgramming #Math
- Central limit theorem in Lean. ~ Rémy Degenne. #ITP #LeanProver #Math
- Prime number theorem and more in Lean. ~ Alex Kontorovich. #ITP #LeanProver #Math
- Formalizing value distribution theory in Lean. ~ Stefan Kebekus. #ITP #LeanProver #Math
- Learn Lean 4 with PLFA (Programming Language Foundations in Agda) proofs. ~ rami3l. #ITP #LeanProver
- Chandra-Furst-Lipton (A digitisation of the number on the forehead model in Lean). ~ Yaël Dillies. #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. #ITP #LeanProver #Math
- Arithmetic progressions - almost periodicity (A digitisation of the Kelley-Meka bound on Roth numbers in Lean). ~ Thomas Bloom, Yaël Dillies. #ITP #LeanProver #Math
- Lecture notes for an introductory course in group theory. ~ Ben Selfridge. #ITP #LeanProver #Math
- Stronger SMT solvers for proof assistants (Proofs, quantifier simplification, strategy schedules). ~ Hans-Jörg Schurr. #ATP #SMT #ITP #IsabelleHOL
- An introduction to typeclass metaprogramming. ~ Alexis King. #Haskell #FunctionalProgramming
- metapredicate declarations. ~ Markus Triska. #Prolog #LogicProgramming
- #Exercitium: Elementos de una matriz con algún vecino menor. #Haskell #ProgramaciónFuncional #Matemáticas
- Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ⊆ u ↔ s ⊆ f⁻¹(u)". #LeanProver #IsabelleHOL #Math #Calculemus
- Curso "Lógica matemática y fundamentos (2011-12)". #Lógica #Haskell #ProgramaciónFuncional