Revisiting an early critique of formal verification. ~ Lawrence Paulson. https://lawrencecpaulson.github.io/2025/03/14/revisiting_demillo.html #ITP #Math #FormalVerification
Revisiting an early critique of formal verification. ~ Lawrence Paulson. https://lawrencecpaulson.github.io/2025/03/14/revisiting_demillo.html #ITP #Math #FormalVerification
La théorie des types, de Russell aux assistans à la demostration. ~ Thierry Coquand. https://www.youtube.com/live/78CQ2A5_EvI #TypeTheory #ITP #Logic #Math
#Calculemus: El problema lógico del mal. https://jaalonso.github.io/calculemus/posts/2020/03/05-el_problema_logico_del_mal #ITP #IsabelleHOL #Lógica
Course notes for "Formalising Mathematics 2025". ~ Bhavik Mehta et als. https://github.com/b-mehta/formalising-mathematics-notes #ITP #LeanProver #Math
LeanAgent: Lifelong learning for formal theorem proving. ~ Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar. https://arxiv.org/abs/2410.06209 #LLMs #ITP #LeanProver #Math
A formal proof of the irrationality of ζ(3) in Lean 4. ~ Junqi Liu, Jujian Zhang, Lihong Zhi. https://arxiv.org/abs/2503.07625 #ITP #LeanProver #Math
Extrinsic termination proofs for well-founded recursion in Lean. ~ Joachim Breitner. https://www.joachim-breitner.de/blog/816-Extrinsic_termination_proofs_for_well-founded_recursion_in_Lean #ITP #LeanProver
The burden of proof: Automated tooling for rapid iteration on large mechanised proofs. ~ Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, John Wickerson. https://www.doc.ic.ac.uk/~afd/papers/2025/FormaliSE.pdf #ITP #IsabelleHOL
Readings shared March 9, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/09-readings_shared_03-09-25 #ITP #LeanProver #Logic #Math #CompSci
Flean: Floating point numbers in Lean, mostly done! ~ Joseph McKinsey. https://josephmckinsey.com/flean2.html #ITP #LeanProver #Math
Floating point numbers in Lean. ~ Joseph McKinsey. https://josephmckinsey.com/flean.html #ITP #LeanProver #Math
#MULCIA: PhD position in number theory and formalization at Vrije Universiteit Amsterdam. https://tinyurl.com/2djc3b7r #PhD #CompSci #ITP #LeanProver