| A formal proof of the Kepler conjecture T Hales, M Adams, G Bauer, TD Dang, J Harrison, H Le Truong, ... Forum of mathematics, Pi 5, e2, 2017 | 483 | 2017 |
| Sphere packings, I TC Hales The Kepler Conjecture: The Hales-Ferguson Proof, 379-431, 2011 | 267* | 2011 |
| A revision of the proof of the Kepler conjecture TC Hales, J Harrison, S McLaughlin, T Nipkow, S Obua, R Zumkeller The Kepler Conjecture: The Hales-Ferguson Proof, 341-376, 2011 | 169 | 2011 |
| Importing hol into isabelle/hol S Obua, S Skalberg Automated Reasoning: Third International Joint Conference, IJCAR 2006 …, 2006 | 90 | 2006 |
| Flyspeck II: the basic linear programs S Obua Technische Universität München, 2008 | 43 | 2008 |
| Proving bounds for real linear programs in Isabelle/HOL S Obua Theorem Proving in Higher Order Logics: 18th International Conference …, 2005 | 38 | 2005 |
| Partizan games in Isabelle/HOLZF S Obua International Colloquium on Theoretical Aspects of Computing, 272-286, 2006 | 33 | 2006 |
| Checking conservativity of overloaded definitions in higher-order logic S Obua International Conference on Rewriting Techniques and Applications, 212-226, 2006 | 20 | 2006 |
| A formal proof of the Kepler conjecture (2015) T Hales, M Adams, G Bauer, DT Dang, J Harrison, TL Hoang, C Kaliszyk, ... Preprint arXiv 1501, 2015 | 14 | 2015 |
| Invariants, modularity, and rights E Cohen, E Alkassar, V Boyarinov, M Dahlweid, U Degenbaev, ... Perspectives of Systems Informatics: 7th International Andrei Ershov …, 2010 | 13 | 2010 |
| ProofPeer: Collaborative theorem proving S Obua, J Fleuriot, P Scott, D Aspinall arXiv preprint arXiv:1404.6186, 2014 | 12 | 2014 |
| A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5 (2017) T Hales, M Adams, G Bauer, TD Dang, J Harrison, LT Hoang, C Kaliszyk, ... URL: https://doi. org/10.1017/fmp, 2017 | 10 | 2017 |
| Type inference for ZFH S Obua, J Fleuriot, P Scott, D Aspinall Intelligent Computer Mathematics: International Conference, CICM 2015 …, 2015 | 6 | 2015 |
| Capturing hiproofs in HOL Light S Obua, M Adams, D Aspinall Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and …, 2013 | 6 | 2013 |
| Proofpeer-a cloud-based interactive theorem proving system S Obua arXiv preprint arXiv:1201.0540, 2012 | 6 | 2012 |
| A formal proof of the Kepler conjecture. CoRR (2015) TC Hales, M Adams, G Bauer, DT Dang, J Harrison, TL Hoang, C Kaliszyk, ... arXiv preprint arXiv:1501.02155, 0 | 4 | |
| Proofscript: Proof scripting for the masses S Obua, P Scott, J Fleuriot Theoretical Aspects of Computing–ICTAC 2016: 13th International Colloquium …, 2016 | 3 | 2016 |
| Local Lexing S Obua, P Scott, J Fleuriot arXiv preprint arXiv:1702.03277, 2017 | 2 | 2017 |
| Proof pearl: looping around the orbit S Obua International Conference on Theorem Proving in Higher Order Logics, 223-231, 2007 | 2 | 2007 |
| Abstraction Logic: A New Foundation for (Computer) Mathematics S Obua arXiv preprint arXiv:2207.05610, 2022 | 1 | 2022 |
