New in Isabelle's Archive of Formal Proofs: Pick's theorem, for finding the area of a simple polygon whose vertices are integral lattice points. It's by Sage Binder and Katherine Kosaian. And it's one of the famous "100 theorems"!
www.isa-afp.org/entries/Pick...
www.isa-afp.org/entries/Pick...
Pick's Theorem
www.isa-afp.org
May 1, 2024 at 1:45 PM
New in Isabelle's Archive of Formal Proofs: Pick's theorem, for finding the area of a simple polygon whose vertices are integral lattice points. It's by Sage Binder and Katherine Kosaian. And it's one of the famous "100 theorems"!
www.isa-afp.org/entries/Pick...
www.isa-afp.org/entries/Pick...
New in the Archive of Formal Proofs: A Modular Formalization of Superposition
by Martin Desharnais and Balazs Toth
Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers.
www.isa-afp.org/entries/Supe...
by Martin Desharnais and Balazs Toth
Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers.
www.isa-afp.org/entries/Supe...
A Modular Formalization of Superposition
www.isa-afp.org
October 31, 2024 at 3:03 PM
New in the Archive of Formal Proofs: A Modular Formalization of Superposition
by Martin Desharnais and Balazs Toth
Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers.
www.isa-afp.org/entries/Supe...
by Martin Desharnais and Balazs Toth
Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers.
www.isa-afp.org/entries/Supe...
New in Isabelle's Archive of Formal Proofs:
Prime Number Theorem with Remainder Term, by Shuhao Song and Bowen Yao.
www.isa-afp.org/entries/PNT_...
Prime Number Theorem with Remainder Term, by Shuhao Song and Bowen Yao.
www.isa-afp.org/entries/PNT_...
www.isa-afp.org
May 8, 2024 at 11:14 AM
New in Isabelle's Archive of Formal Proofs:
Prime Number Theorem with Remainder Term, by Shuhao Song and Bowen Yao.
www.isa-afp.org/entries/PNT_...
Prime Number Theorem with Remainder Term, by Shuhao Song and Bowen Yao.
www.isa-afp.org/entries/PNT_...
Go Code Generation for Isabelle - Archive of Formal Proofs www.isa-afp.org/entries/Go.h...
March 12, 2024 at 5:01 AM
Go Code Generation for Isabelle - Archive of Formal Proofs www.isa-afp.org/entries/Go.h...
New in the Archive of Formal Proofs:
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality
by Ievgen Ivanov
The decreasing diagrams method is complete for proving confluence of relations of the least uncountable cardinality.
www.isa-afp.org/entries/Comp...
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality
by Ievgen Ivanov
The decreasing diagrams method is complete for proving confluence of relations of the least uncountable cardinality.
www.isa-afp.org/entries/Comp...
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality in the Archive of Formal Proofs
www.isa-afp.org
April 13, 2025 at 9:44 AM
New in the Archive of Formal Proofs:
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality
by Ievgen Ivanov
The decreasing diagrams method is complete for proving confluence of relations of the least uncountable cardinality.
www.isa-afp.org/entries/Comp...
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality
by Ievgen Ivanov
The decreasing diagrams method is complete for proving confluence of relations of the least uncountable cardinality.
www.isa-afp.org/entries/Comp...
Check out the #isabelle-hol formalization of the core contribution from my thesis in the #archive-of-formal-proofs! Computer-says 🤖: Ben's math is correct! ✅
www.isa-afp.org/entries/Weak...
www.isa-afp.org/entries/Weak...
The Weak Spectroscopy Game to Characterize Behavioral Equivalences
The Weak Spectroscopy Game to Characterize Behavioral Equivalences in the Archive of Formal Proofs
www.isa-afp.org
November 24, 2025 at 10:24 AM
Check out the #isabelle-hol formalization of the core contribution from my thesis in the #archive-of-formal-proofs! Computer-says 🤖: Ben's math is correct! ✅
www.isa-afp.org/entries/Weak...
www.isa-afp.org/entries/Weak...
Distributed parallel build for the Isabelle Archive of Formal Proofs. ~ Fabian Huch & Makarius Wenzel. drops.dagstuhl.de/storage/00li... #ITP #IsabelleHOL
September 6, 2024 at 12:11 PM
Distributed parallel build for the Isabelle Archive of Formal Proofs. ~ Fabian Huch & Makarius Wenzel. drops.dagstuhl.de/storage/00li... #ITP #IsabelleHOL
Set theory with types
Set theory with types 21 Nov 2025 [ AUTOMATH NG de Bruijn type theory set theory type classes Principia Mathematica Archive of Formal Proofs ] It is known that mathematics is heavily reliant on set theory, but no one can agree on what set theory is. Many people today…
Set theory with types 21 Nov 2025 [ AUTOMATH NG de Bruijn type theory set theory type classes Principia Mathematica Archive of Formal Proofs ] It is known that mathematics is heavily reliant on set theory, but no one can agree on what set theory is. Many people today…
Set theory with types
Set theory with types 21 Nov 2025 [ AUTOMATH NG de Bruijn type theory set theory type classes Principia Mathematica Archive of Formal Proofs ] It is known that mathematics is heavily reliant on set theory, but no one can agree on what set theory is. Many people today understand that we have a choice between set theory and type theory, but they don’t know what type theory is either. Many think that type theory refers to some sort of dependent type theory, as found in Lean or Agda, while everything else is set theory.
cnznews.com
November 24, 2025 at 10:52 AM
Set theory with types
Set theory with types 21 Nov 2025 [ AUTOMATH NG de Bruijn type theory set theory type classes Principia Mathematica Archive of Formal Proofs ] It is known that mathematics is heavily reliant on set theory, but no one can agree on what set theory is. Many people today…
Set theory with types 21 Nov 2025 [ AUTOMATH NG de Bruijn type theory set theory type classes Principia Mathematica Archive of Formal Proofs ] It is known that mathematics is heavily reliant on set theory, but no one can agree on what set theory is. Many people today…
New in Isabelle's Archive of Formal Proofs: Kummer's congruence
www.isa-afp.org/entries/Kumm...
www.isa-afp.org/entries/Kumm...
March 29, 2024 at 12:49 PM
New in Isabelle's Archive of Formal Proofs: Kummer's congruence
www.isa-afp.org/entries/Kumm...
www.isa-afp.org/entries/Kumm...
We've now wrapped up Day 2 & Session 4 of #LoveDataWeek! 🎉 A big thank you to Jordan Byers (HEPData), Fabian Huch (Archive of Formal Proofs), and Aleksandra Wilczynska (4TU.ResearchData) for their insights on making research data FAIR in high energy physics, math, engineering & design
February 11, 2025 at 3:04 PM
We've now wrapped up Day 2 & Session 4 of #LoveDataWeek! 🎉 A big thank you to Jordan Byers (HEPData), Fabian Huch (Archive of Formal Proofs), and Aleksandra Wilczynska (4TU.ResearchData) for their insights on making research data FAIR in high energy physics, math, engineering & design
New in the Archive of Formal Proofs:
The Uncertainty Principle, by Alexander Treml A formal proof of the uncertainty principle known from quantum mechanics, based upon work on complex vector spaces .
www.isa-afp.org/entries/Unce...
The Uncertainty Principle, by Alexander Treml A formal proof of the uncertainty principle known from quantum mechanics, based upon work on complex vector spaces .
www.isa-afp.org/entries/Unce...
April 8, 2024 at 11:00 AM
New in the Archive of Formal Proofs:
The Uncertainty Principle, by Alexander Treml A formal proof of the uncertainty principle known from quantum mechanics, based upon work on complex vector spaces .
www.isa-afp.org/entries/Unce...
The Uncertainty Principle, by Alexander Treml A formal proof of the uncertainty principle known from quantum mechanics, based upon work on complex vector spaces .
www.isa-afp.org/entries/Unce...