Follow
Steven Obua
Title
Cited by
Cited by
Year
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, 2017
3422017
Sphere packings, I
TC Hales
The Kepler Conjecture, 379-431, 2011
255*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, 341-376, 2011
1542011
Importing hol into isabelle/hol
S Obua, S Skalberg
International Joint Conference on Automated Reasoning, 298-302, 2006
892006
Flyspeck II: the basic linear programs
S Obua
Technische Universität München, 2008
412008
Proving bounds for real linear programs in Isabelle/HOL
S Obua
International Conference on Theorem Proving in Higher Order Logics, 227-244, 2005
332005
Partizan games in Isabelle/HOLZF
S Obua
International Colloquium on Theoretical Aspects of Computing, 272-286, 2006
232006
Checking conservativity of overloaded definitions in higher-order logic
S Obua
International Conference on Rewriting Techniques and Applications, 212-226, 2006
192006
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
142015
Invariants, modularity, and rights
E Cohen, E Alkassar, V Boyarinov, M Dahlweid, U Degenbaev, ...
International Andrei Ershov Memorial Conference on Perspectives of System …, 2009
142009
ProofPeer: Collaborative theorem proving
S Obua, J Fleuriot, P Scott, D Aspinall
arXiv preprint arXiv:1404.6186, 2014
112014
Capturing hiproofs in hol light
S Obua, M Adams, D Aspinall
International Conference on Intelligent Computer Mathematics, 184-199, 2013
62013
Proofpeer-a cloud-based interactive theorem proving system
S Obua
arXiv preprint arXiv:1201.0540, 2012
62012
Type inference for ZFH
S Obua, J Fleuriot, P Scott, D Aspinall
International Conference on Intelligent Computer Mathematics, 87-101, 2015
52015
Proofscript: Proof scripting for the masses
S Obua, P Scott, J Fleuriot
International Colloquium on Theoretical Aspects of Computing, 333-348, 2016
32016
Proof pearl: looping around the orbit
S Obua
International Conference on Theorem Proving in Higher Order Logics, 223-231, 2007
22007
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
2
Bootstrapping LCF Declarative Proofs
P Scott, S Obua, J Fleuriot
arXiv preprint arXiv:1703.05351, 2017
12017
Local Lexing
S Obua, P Scott, J Fleuriot
arXiv preprint arXiv:1702.03277, 2017
12017
Social Network Processes in the Isabelle and Coq Theorem Proving Communities
J Fleuriot, S Obua, P Scott
arXiv preprint arXiv:1609.07127, 2016
12016
The system can't perform the operation now. Try again later.
Articles 1–20