Editing Proof assistant (section)

== Notable formalized proofs ==

{{See also|Computer-assisted proof#Theorems proved with the help of computer programs}}

The following is a list of notable proofs that have been formalized within proof assistants.

{| class=wikitable
! scope="col" | Theorem
! scope="col" | Proof assistant
! scope="col" | Year
|-
| [[Four color theorem]]<ref>{{Citation |last=Gonthier |first=Georges |author-link=Georges Gonthier |title=Formal Proof—The Four-Color Theorem |journal=[[Notices of the American Mathematical Society]] |volume=55 |year=2008 |url=https://www.ams.org/notices/200811/tx081101382p.pdf |archive-url=https://web.archive.org/web/20110805094909/http://www.ams.org/notices/200811/tx081101382p.pdf |archive-date=2011-08-05 |url-status=live |issue=11 |pages=1382–1393 |mr=2463991 }}</ref> || Coq || 2005
|-
| [[Feit–Thompson theorem]]<ref>{{Cite web |date=2016-11-19 |title=Feit thomson proved in coq - Microsoft Research Inria Joint Centre |url=http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ |access-date=2023-12-07 |archive-url=https://web.archive.org/web/20161119094854/http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ |archive-date=2016-11-19 }}</ref> || Coq || 2012
|-
| [[Fundamental group]] of the [[circle]]<ref>{{Cite book |title=2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science |url=https://ieeexplore.ieee.org/document/6571554 |access-date=2023-12-07 |doi=10.1109/lics.2013.28 |date=2013 |last1=Licata |first1=Daniel R. |last2=Shulman |first2=Michael |chapter=Calculating the Fundamental Group of the Circle in Homotopy Type Theory |pages=223–232 |arxiv=1301.3443 |isbn=978-1-4799-0413-6 |s2cid=5661377 }}</ref> || Coq || 2013
|-
|[[Erdős–Graham problem]]<ref>{{Cite web |date=2022-03-11 |title=Math Problem 3,500 Years In The Making Finally Gets A Solution |url=https://www.iflscience.com/math-problem-3500-years-in-the-making-finally-gets-a-solution-62925 |access-date=2024-02-09 |website=IFLScience |language=en}}</ref><ref>{{Cite arXiv |last=Avigad |first=Jeremy |date=2023 |class=math.HO |title=Mathematics and the formal turn |eprint=2311.00007 }}</ref>
|Lean
|2022
|- 
| Polynomial Freiman-Ruzsa conjecture over <math>\mathbb F_2</math><ref>{{Cite web |last=Sloman |first=Leila |date=2023-12-06 |title='A-Team' of Math Proves a Critical Link Between Addition and Sets |url=https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/ |access-date=2023-12-07 |website=Quanta Magazine |language=en}}</ref> || Lean || 2023
|-
|[[Busy Beaver|BB(5)]] = 47,176,870<ref>{{Cite web |date=2024-07-02 |title=We have proved "BB(5) = 47,176,870" |url=https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 |access-date=2024-07-09 |website=The Busy Beaver Challenge |language=en}}</ref>
|Coq
|2024
|}