papers
Publications (4)
math.LO2012
Some new results on decidability for elementary algebra and geometry
Robert M. Solovay, R. D. Arthan, John Harrison
cs.AI2006
LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)
Christoph Benzmueller, John Harrison, Carsten Schuermann
math.MG2009
A revision of the proof of the Kepler conjecture
Thomas C. Hales, John Harrison, Sean McLaughlin +3
math.MG2015
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer +19