#proofassistants — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #proofassistants, aggregated by home.social.
-
Books on automated #ProofAssistants, like Coq, Lean, Agda, Idris, etc., fall into two groups: a vast majority aimed at working mathematicians and a handful aimed at programmers.
The following is a short list of #programming-focused #books (not short tutorials) on the use of proof assistants in crafting #verified software, categorised by type theory and listed in an approximate, ascending order of sophistication:
\(\textit{Coquand Calculus of Inductive Constructions}\)
• Introduction to Formal Reasoning (Lean), Altenkirch
• Programs and Proofs (Coq), Sergey
• Functional Programming in Lean, Christiansen
• Verified Functional Algorithms (Coq), Appel
• Certified Programming with Dependent Types (Coq), Chlipala\(\textit{Martin-Löf Intuitionistic Type Theory}\)
• Certainty by Construction (Agda), Maguire
• Type-Driven Development with Idris, Brady
• Verified Functional Programming in Agda, Stump
• Programming Language Foundations in Agda, Wadler
• Software Foundations (Idris ed), Piercehttps://idris-hackers.github.io/software-foundations/pdf/sf-idris-2018.pdf
-
Books on automated #ProofAssistants, like Coq, Lean, Agda, Idris, etc., fall into two groups: a vast majority aimed at working mathematicians and a handful aimed at programmers.
The following is a short list of #programming-focused #books (not short tutorials) on the use of proof assistants in crafting #verified software, categorised by type theory and listed in an approximate, ascending order of sophistication:
\(\textit{Coquand Calculus of Inductive Constructions}\)
• Introduction to Formal Reasoning (Lean), Altenkirch
• Programs and Proofs (Coq), Sergey
• Functional Programming in Lean, Christiansen
• Verified Functional Algorithms (Coq), Appel
• Certified Programming with Dependent Types (Coq), Chlipala\(\textit{Martin-Löf Intuitionistic Type Theory}\)
• Certainty by Construction (Agda), Maguire
• Type-Driven Development with Idris, Brady
• Verified Functional Programming in Agda, Stump
• Programming Language Foundations in Agda, Wadler
• Software Foundations (Idris ed), Piercehttps://idris-hackers.github.io/software-foundations/pdf/sf-idris-2018.pdf
-
This is my #Lean 4 #proof of the nonexistence of #God, based on "§2.4 Modeling English Propositions" p.37 of "A Logical Approach to Discrete Mathematics" by Gries and Schneider (1993):
• If God were able and willing to prevent evil, He would do so:
Able ∧ Willing → Prevents
• If God were unable to prevent evil, He would be impotent:
¬Able → Impotent
• If God were unwilling to prevent evil, He would be malevolent:
¬Willing → Malevolent
• God does not prevent evil:
¬Prevents
• If God exists, He is neither impotent nor malevolent:
GodExists → ¬Impotent ∧ ¬Malevolent
• Therefore, God does not exist:
¬GodExistsShed no tears for me, were I to end up in #Hell. That my code type checks in Lean 4 at all is a little bit of #Heaven for me.
-
This is my #Lean 4 #proof of the nonexistence of #God, based on "§2.4 Modeling English Propositions" p.37 of "A Logical Approach to Discrete Mathematics" by Gries and Schneider (1993):
• If God were able and willing to prevent evil, He would do so:
Able ∧ Willing → Prevents
• If God were unable to prevent evil, He would be impotent:
¬Able → Impotent
• If God were unwilling to prevent evil, He would be malevolent:
¬Willing → Malevolent
• God does not prevent evil:
¬Prevents
• If God exists, He is neither impotent nor malevolent:
GodExists → ¬Impotent ∧ ¬Malevolent
• Therefore, God does not exist:
¬GodExistsShed no tears for me, were I to end up in #Hell. That my code type checks in Lean 4 at all is a little bit of #Heaven for me.
-
After 50 years of "progress," proof assistants are still just glorified calculators for people who think typing "Isabelle Coq" makes them sound smart. 🤓🔧 It's the same old story of academia's perpetual quest to turn #math into a spectator sport—except this game has fewer fans than a #calculus lecture. 🥱📉
https://lawrencecpaulson.github.io//2025/12/05/History_of_Proof_Assistants.html #proofassistants #academia #humor #IsabelleCoq #spectatorSport #HackerNews #ngated -
After 50 years of "progress," proof assistants are still just glorified calculators for people who think typing "Isabelle Coq" makes them sound smart. 🤓🔧 It's the same old story of academia's perpetual quest to turn #math into a spectator sport—except this game has fewer fans than a #calculus lecture. 🥱📉
https://lawrencecpaulson.github.io//2025/12/05/History_of_Proof_Assistants.html #proofassistants #academia #humor #IsabelleCoq #spectatorSport #HackerNews #ngated -
Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!
The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!
Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!
-
Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!
The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!
Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!
-
Formal verification of leftist and skew heaps in Rocq. ~ Elena Marcela Dumitrache. https://fse.studenttheses.ub.rug.nl/36519/1/bCS2025DumitracheEM.pdf #FormalVerification #ProofAssistants #Rocq
-
Formal verification of leftist and skew heaps in Rocq. ~ Elena Marcela Dumitrache. https://fse.studenttheses.ub.rug.nl/36519/1/bCS2025DumitracheEM.pdf #FormalVerification #ProofAssistants #Rocq
-
Algorithmic conversion with surjective pairing: A syntactic and untyped approach. ~ Yiyun Liu, Stephanie Weirich. https://electriclam.com/papers/conf.pdf #FormalVerification #ProofAssistants #CoqProver
-
Algorithmic conversion with surjective pairing: A syntactic and untyped approach. ~ Yiyun Liu, Stephanie Weirich. https://electriclam.com/papers/conf.pdf #FormalVerification #ProofAssistants #CoqProver
-
Verified functional graph algorithms using the Rocq prover (Coq). ~ Leopold Frieberger. https://fse.studenttheses.ub.rug.nl/36509/1/Bachelors-Thesis-Leopold-Frieberger-Repository.pdf #FormalVerification #ProofAssistants #Rocq
-
Verified functional graph algorithms using the Rocq prover (Coq). ~ Leopold Frieberger. https://fse.studenttheses.ub.rug.nl/36509/1/Bachelors-Thesis-Leopold-Frieberger-Repository.pdf #FormalVerification #ProofAssistants #Rocq
-
Formal verification of pairing heaps in Rocq. ~ Cosmin-Ionut Visan. https://fse.studenttheses.ub.rug.nl/36504/1/bCS2025VisanCI.pdf #FormalVerification #ProofAssistants #Rocq
-
Formal verification of pairing heaps in Rocq. ~ Cosmin-Ionut Visan. https://fse.studenttheses.ub.rug.nl/36504/1/bCS2025VisanCI.pdf #FormalVerification #ProofAssistants #Rocq
-
Formal verification of the safegcd implementation. ~ Russell O'Connor, Andrew Poelstra. https://arxiv.org/abs/2507.17956 #FormalVerification #ProofAssistants #CoqProver
-
Formal verification of the safegcd implementation. ~ Russell O'Connor, Andrew Poelstra. https://arxiv.org/abs/2507.17956 #FormalVerification #ProofAssistants #CoqProver
-
Reseña de «Solving formal math problems by decomposition and iterative reflection». https://jaalonso.github.io/vestigium/posts/2025/07/27-solving-formal-math-problems-by-decomposition-and-iterative-reflection/ #AI4Math #LLMs #ProofAssistants #LeanProver #Math
-
Reseña de «Solving formal math problems by decomposition and iterative reflection». https://jaalonso.github.io/vestigium/posts/2025/07/27-solving-formal-math-problems-by-decomposition-and-iterative-reflection/ #AI4Math #LLMs #ProofAssistants #LeanProver #Math
-
Solving formal math problems by decomposition and iterative reflection. Yichi Zhou et als. https://arxiv.org/abs/2507.15225v1 #AI4Math #LLMs #ProofAssistants #LeanProver #Math
-
Solving formal math problems by decomposition and iterative reflection. Yichi Zhou et als. https://arxiv.org/abs/2507.15225v1 #AI4Math #LLMs #ProofAssistants #LeanProver #Math
-
Formally verified suffix array construction (in Isabelle/HOL). ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. https://link.springer.com/article/10.1007/s10817-025-09735-8 #FormalVerification #ProofAssistants #IsabelleHOL #Haskell #FunctionalProgramming
-
Formally verified suffix array construction (in Isabelle/HOL). ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. https://link.springer.com/article/10.1007/s10817-025-09735-8 #FormalVerification #ProofAssistants #IsabelleHOL #Haskell #FunctionalProgramming
-
McTT: A verified kernel for a proof assistant. ~ Junyoung Jang et als. https://hustmphrrr.github.io/asset/papers/icfp25-mctt.pdf #ProofAssistants #Rocq
-
McTT: A verified kernel for a proof assistant. ~ Junyoung Jang et als. https://hustmphrrr.github.io/asset/papers/icfp25-mctt.pdf #ProofAssistants #Rocq
-
Autoformalization of mathematical theorems? No shit!
—
New blog post on Freedom Math Dancehttps://freedommathdance.blogspot.com/2025/07/autoformalization-of-mathematical.html
-
Autoformalization of mathematical theorems? No shit!
—
New blog post on Freedom Math Dancehttps://freedommathdance.blogspot.com/2025/07/autoformalization-of-mathematical.html
-
Join our discussion on #proofs and #proofAssistants in our latest episode of it’s not just numbers! And don’t forget to look at the links in the show notes if you want to try them out
You can find the episode on https://creators.spotify.com/pod/show/not-just-numbers/episodes/S2E06---Proofs-and-proof-assistants-with-Sander-Dahmen-and-Jim-Portegies-e31knov or your favourite podcast platform
-
With the NWO XL consortium on Cyclic Structures in Programs and Proofs, we are looking for 6 highly motivated and talented PhD students starting in September (with some flexibility).
The topics range from Modal logic, proof theory, and coalgebras to Programming languages, concurrency, and type systems and Proof assistants (#Agda, #Rocq).
Information about the positions and application procedure can be found on the website:
cyclic-structures.gitlab.io/vacancies/
Applications will be evaluated on a rolling basis but should be submitted by the 23rd of May for full consideration.
Please forward to any strong candidates you know!
#TypeTheory #ModalLogic #Concurrency #ProgrammingLanguages #TypeSystems #ProofAssistants #CyclicStructures #PhD #Netherlands #UniversityOfGroningen #LeidenUniversity #UniversityOfTwente #TUDelft #RadboudUniversity -
With the NWO XL consortium on Cyclic Structures in Programs and Proofs, we are looking for 6 highly motivated and talented PhD students starting in September (with some flexibility).
The topics range from Modal logic, proof theory, and coalgebras to Programming languages, concurrency, and type systems and Proof assistants (#Agda, #Rocq).
Information about the positions and application procedure can be found on the website:
cyclic-structures.gitlab.io/vacancies/
Applications will be evaluated on a rolling basis but should be submitted by the 23rd of May for full consideration.
Please forward to any strong candidates you know!
#TypeTheory #ModalLogic #Concurrency #ProgrammingLanguages #TypeSystems #ProofAssistants #CyclicStructures #PhD #Netherlands #UniversityOfGroningen #LeidenUniversity #UniversityOfTwente #TUDelft #RadboudUniversity -
As part of our (@[email protected] and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.
We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.
Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS
You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).
P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.
#Agda #Coq #Rocq #Lean #LiquidHaskell #Rust #Haskell #TypeDrivenDevelopment #TyDe #DependentTypes #LiquidTypes #RefinementTypes #ProofAssistants #Survey
-
As part of our (@[email protected] and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.
We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.
Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS
You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).
P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.
#Agda #Coq #Rocq #Lean #LiquidHaskell #Rust #Haskell #TypeDrivenDevelopment #TyDe #DependentTypes #LiquidTypes #RefinementTypes #ProofAssistants #Survey
-
Call for Papers
16th International Conference on Interactive Theorem Proving — ITP'25Reykjavik, Iceland
27 September – 3 October 2025https://icetcs.github.io/frocos-itp-tableaux25/itp/
ITP is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.
- Abstract submission deadline: 12 March 2025
- Paper submission deadline: 19 March 2025
- Author notification: 23 May 2025
- Camera-ready copy due: 27 June 2025#formalization #theoremproving #proofassistants #verification #CfP
-
Call for Papers
16th International Conference on Interactive Theorem Proving — ITP'25Reykjavik, Iceland
27 September – 3 October 2025https://icetcs.github.io/frocos-itp-tableaux25/itp/
ITP is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.
- Abstract submission deadline: 12 March 2025
- Paper submission deadline: 19 March 2025
- Author notification: 23 May 2025
- Camera-ready copy due: 27 June 2025#formalization #theoremproving #proofassistants #verification #CfP
-
Registration for the Midlands Graduate School (MGS) in the Foundations of Computing Science is now open!
Spaces are limited, so please register early to secure your place.
https://tinyurl.com/MGS-2025#categorytheory #typetheory #logic #proofassistants #quantumcomputing
-
The #software that control avionics, ATC systems, medical devices, and other #LifeCritical systems should be implemented in modern #ProofAssistants, like Lean, Coq, Asda, Idris, etc.
A failure of the control software in a medical device may kill one person. A failure of the avionics software in a commercial airliner may kill hundreds. A failure of the ATC software may kill thousands.
Still, these failures are quantifiable. By a stark contrast, a failure of an infrastructural software, like #CrowdStrike or #Windows may well cause the loss of countless lives, limbs, and lollies.
So, using PowerShell, Bash, JavaScript, Python, and other expedient, popular languages to mash together an infrastructural system is not only inadvisable, it is outright insupportable.
-
Lecturas compartidas el 18 de marzo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-18-de-marzo #AI #ATP #Coq #FunctionalProgramming #HOL_Light #Haskell #ITP #IsabelleHOL #LLMs #Lean4 #LeanProver #MachineLearning #Math #ProofAssistants
-
Machine assisted proofs. ~ Terence Tao (@tao). https://terrytao.files.wordpress.com/2024/03/machine-assisted-proof-notices.pdf #ITP #ProofAssistants #Coq #IsabelleHOL #HOL_Light #LeanProver #MachineLearning #LLMs #Math
-
Machine assisted proofs [Slides]. ~ Terence Tao (@tao). https://terrytao.files.wordpress.com/2024/03/machine-jan-3.pdf #ITP #ProofAssistants #Coq #IsabelleHOL #HOL_Light #LeanProver #MachineLearning #LLMs #Math
