Readings shared May 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/10-readings_shared_05-10-25 #ITP #LeanProver #Math #Mathlib #Python

Readings shared May 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/10-readings_shared_05-10-25 #ITP #LeanProver #Math #Mathlib #Python
LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. https://www.leanexplore.com/ #ITP #LeanProver #Mathlib
A tool to verify estimates, II: a flexible proof assistant. ~Terence Tao. https://terrytao.wordpress.com/2025/05/09/a-tool-to-verify-estimates-ii-a-flexible-proof-assistant/ #ITP #Python #Math
How to (actually) prove it - New frontiers of mathematics & computing in Lean. ~ Kiran. https://kirancodes.me/posts/log-how-to-prove-it-maths.html #ITP #LeanProver #Math
Lógicas de orden superior y verificación formal [Slides]. ~ Lourdes del Carmen González Huesca. https://drive.google.com/drive/folders/1cE1a0N-2ZMrVx8i58W0KG8s3KMVHawZn #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
Lógicas de orden superior y verificación formal. ~ Lourdes del Carmen González Huesca. https://youtu.be/9uTD7BMvbjw #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
ProofBuddy (How it started, how it's going). ~ Nadine Karsten, Kim Jana Eiken, Uwe Nestmann. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.6.pdf #ITP #IsabelleHOL #Logic #Teaching
Minimal sequent calculus for teaching first-order logic: Lessons learned. ~ Jørgen Villadsen. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.5.pdf #ITP #IsabelleHOL #Logic #Teaching
OnlineProver: Experience with a visualisation tool for teaching formal proofs. ~ Ján Perháč et als. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.4.pdf #ITP #Logic #Teaching
A graphical interface for category theory proofs in Coq. ~ Luc Chabassier. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.2.pdf #ITP #Coq #Rocq #CategoryTheory
Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord and Julien Narboux. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.1.pdf #ATP #ITP #IsabelleHOL #LeanProver #Coq #Rocq #Education
Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. https://arxiv.org/abs/2505.05362 #ITP #Coq #Rocq
Lean4 machine assisted proof framework for chip firing game & graphical Riemann-Roch. ~ Dhyey Dharmendrakumar Mavani. https://dhyeymavani.com/publication/math-thesis-lean/math-thesis-lean.pdf #ITP #LeanProver
Beyond theorem proving: Formulation, framework and benchmark for formal problem-solving. ~ Qi Liu et als. https://arxiv.org/abs/2505.04528 #LLMs #ITP #LeanProver
FormalMATH: Benchmarking formal mathematical reasoning of large language models. ~ Zhouliang Yu et als. https://arxiv.org/abs/2505.02735 #LLMs #Autoformalization #Math #ITP #LeanProver
Readings shared May 6, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/06-readings_shared_05-06-25 #Emacs #ITP #IsabelleHOL #Math #Python