Developments in Formal Proofs

Thomas C. Hales

Type: Preprint

Publication Date: 2014-08-24

Citations: 13

Locations

arXiv (Cornell University) - View

Similar Works

Action	Title	Year	Authors
+	Developments in Formal Proofs	2014	Thomas C. Hales
+	Reliably Reproducing Machine-Checked Proofs with the Coq Platform	2022	Karl Palmskog E. ̃Tassi Théo Zimmermann
+	Comparison of Two Theorem Provers: Isabelle/HOL and Coq	2018	Artem Yushkovskiy
+	Comparison of Two Theorem Provers: Isabelle/HOL and Coq.	2018	Artem Yushkovskiy Stavros Tripakis
+	From LCF to Isabelle/HOL	2019	Lawrence C. Paulson Tobias Nipkow Makarius Wenzel
+ PDF Chat	From LCF to Isabelle/HOL	2019	Lawrence C. Paulson Tobias Nipkow Makarius Wenzel
+ PDF Chat	Proust: A Nano Proof Assistant	2016	Prabhakar Ragde
+ PDF Chat	General Automation in Coq through Modular Transformations	2021	Valentin Blot Louise Dubois de Prisque Chantal Keller Pierre Vial
+	General Automation in Coq through Modular Transformations	2021	Valentin Blot Louise Dubois de Prisque Chantal Keller Pierre Vial
+	Isabelle: The Next 700 Theorem Provers	1993	Lawrence C. Paulson
+	Isabelle technology for the Archive of Formal Proofs.	2019	Makarius Wenzel
+ PDF Chat	Teaching Higher-Order Logic Using Isabelle	2024	Simon Tobias Lund Jørgen Villadsen
+ PDF Chat	Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started	2020	Angeliki Koutsoukou-Argyraki
+	QED at Large: A Survey of Engineering of Formally Verified Software	2019	Talia Ringer Karl Palmskog Ilya Sergey Milos Gligoric Zachary Tatlock
+	Exposé Bourbaki 1086 : Developments in formal proofs	2018	Thomas C. Hales
+ PDF Chat	QED at Large: A Survey of Engineering of Formally Verified Software	2019	Talia Ringer Karl Palmskog Ilya Sergey Milos Gligoric Zachary Tatlock
+ PDF Chat	A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving	2012	Freek Wiedijk
+	Interaction with Formal Mathematical Documents in Isabelle/PIDE	2019	Makarius Wenzel
+	Interaction with Formal Mathematical Documents in Isabelle/PIDE	2019	Makarius Wenzel
+	Formal Proof of Higman's Lemma on Isabelle/HOL	2012	Mizuhito Ogawa

Works That Cite This (6)

Action	Title	Year	Authors
+ PDF Chat	A FORMAL PROOF OF THE KEPLER CONJECTURE	2017	Thomas Hales Mark Adams Gertrud Bauer TAT DAT DANG John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron Sean McLaughlin TAT THANG NGUYEN
+ PDF Chat	A Survey of Languages for Formalizing Mathematics	2020	Cezary Kaliszyk Florian Rabe
+	A Survey of Languages for Formalizing Mathematics	2020	Cezary Kaliszyk Florian Rabe
+	A formal proof of the Kepler conjecture	2015	Thomas Hales Mark Adams Gertrud Bauer Dat Tat Dang John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron Sean McLaughlin Thang Tat Nguyen
+ PDF Chat	Goal Translation for a Hammer for Coq (Extended Abstract)	2016	Łukasz Czajka Cezary Kaliszyk
+ PDF Chat	DeepAlgebra - An Outline of a Program	2017	Przemysław Chojecki

Works Cited by This (13)

Action	Title	Year	Authors
+	The Kepler conjecture	1998	Thomas C. Hales
+	SOLVABILITY OF GROUPS OF ODD ORDER	2012	Walter Feit John G. Thompson John G. Thompson
+	Finite groups in which the centralizer of any non-identity element is nilpotent	1960	Walter Feit Marshall Hall John G. Thompson
+ PDF Chat	Formalizing an Analytic Proof of the Prime Number Theorem	2009	John Harrison
+ PDF Chat	Nonsolvable finite groups all of whose local subgroups are solvable	1968	John G. Thompson
+	The Simplicial Model of Univalent Foundations (after Voevodsky)	2012	Chris Kapulkin Peter LeFanu Lumsdaine
+ PDF Chat	Homotopy type theory and Voevodsky’s univalent foundations	2014	Álvaro Pelayo Michael A. Warren
+ PDF Chat	Homotopy theoretic models of identity types	2008	Steve Awodey Michael A. Warren
+	A new look at the Feit-Thompson odd order theorem	1999	Geoge Glauberman
+	A formally verified proof of the Central Limit Theorem	2014	Jeremy Avigad Johannes Hölzl Luke Serafin