Advancing mathematics research with AI-driven formal proof search. ~ George Tsoukalas et als. arxiv.org/abs/2605.22763
@jalonso.eurosky.social
@jalonso.eurosky.socialAdvancing mathematics research with AI-driven formal proof search. ~ George Tsoukalas et als. arxiv.org/abs/2605.22763
@jalonso.eurosky.socialZFLean: a Lean 4 library for doing core mathematics inside Mathlib's model of ZFC set theory. ~ Vincent Trélat, Matteo Pouillat. github.com/VTrelat/ZFLean
@jalonso.eurosky.socialZFLean: a framework for set-level mathematics in Lean. ~ Vincent Trélat, Matteo Pouillat. arxiv.org/abs/2604.24195
@jalonso.eurosky.socialFormally certifying the vertex set of a polyhedron faster than informal enumeration. ~ Xavier Allamigeon, Yazid Id-Sahra, Pierre-Yves Strub. arxiv.org/abs/2610.11913
@jalonso.eurosky.socialAIProver: agentic auto-formalization of mathematical research via certificate-driven evolving harness. ~ Prithwish Jana et als. arxiv.org/abs/2610.053...
@jalonso.eurosky.socialA Lean~4 framework for the radii polynomial method. ~ Fengyang Wang. arxiv.org/abs/2610.023...
@jalonso.eurosky.socialToward a Lean formalization of analog computing with microwaves. ~ Matteo Nerini, Xuekang Liu, Bruno Clerckx. arxiv.org/abs/2610.047... #LeanProver #ITP
@jalonso.eurosky.socialErdős 374: classical square products of factorials (in Lean 4). ~ Alexander. palomar-registry.org/entry?id=PAL... #LeanProver #ITP #Math
@jalonso.eurosky.socialSoftware Foundations In Lean. ~ Benjamin Pierce et als. www.renaissancephilanthropy.org/software-fou...
@jalonso.eurosky.socialThe Steiner deltoid as the tangent envelope of Wallace-Simson Lines in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Stei...
@jalonso.eurosky.socialSteiner's line theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Stei...
@jalonso.eurosky.socialMathematical proof assistants for teaching logic: the LogiKEy methodology. ~ Christoph Benzmüller, David Fuenmayor, Luca Pasetto. arxiv.org/abs/2610.08214
@jalonso.eurosky.socialA first introduction to Isabelle/ML metaprogramming: automatic estimation of polynomial degrees. ~ Jonas Bayer, Anna Danilkin, Marco David, Annie Yao. arxiv.org/abs/2610.08359 #IsabelleHOL #ITP
@jalonso.eurosky.socialAn AI-assisted formalization of the Poincaré conjecture. ~ Zhiyuan Zhang, Axel Delaval, Leheng Chen, Jinxuan Chen, Jie Xu, Yuxuan Liao, Jiedong Jiang, Chunlei Liu, Bin Dong. arxiv.org/abs/2610.083...
@jalonso.eurosky.socialLeanAutoformalizationSkills: A collection of skills for using Codex or Claude Code to formalize mathematics in Lean 4. ~ Scott Armstrong. github.com/scottnarmstr...
@jalonso.eurosky.socialAutoformalization is now very easy. ~ Scott Armstrong. www.scottnarmstrong.com/2026/10/auto... #LeanProver #ITP #AI4Math #Autoformalization
@jalonso.eurosky.socialEnunciado del reto 22 de Lean 4: Si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente. jaalonso.github.io/calculemus/p... #RetoLean4
@jalonso.eurosky.socialEnunciado del reto 22 de Lean 4: Si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente.
@jalonso.eurosky.socialSoluciones del reto 21 de Lean 4: Las subsucesiones tienen el mismo límite que la sucesión. jaalonso.github.io/calculemus/p...
@jalonso.eurosky.socialWeekly reads: Sep 28 – Oct 4, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Agda #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver