Suivre
Steven Obua
Titre
Citée par
Citée par
Année
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
4432017
Sphere packings, I
TC Hales
The Kepler Conjecture: The Hales-Ferguson Proof, 379-431, 2011
261*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
2082011
Importing hol into isabelle/hol
S Obua, S Skalberg
Automated Reasoning: Third International Joint Conference, IJCAR 2006 …, 2006
892006
Flyspeck II: the basic linear programs
S Obua
Technische Universität München, 2008
422008
Proving bounds for real linear programs in Isabelle/HOL
S Obua
Theorem Proving in Higher Order Logics: 18th International Conference …, 2005
382005
Partizan games in Isabelle/HOLZF
S Obua
International Colloquium on Theoretical Aspects of Computing, 272-286, 2006
322006
Checking conservativity of overloaded definitions in higher-order logic
S Obua
International Conference on Rewriting Techniques and Applications, 212-226, 2006
202006
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
132015
Invariants, modularity, and rights
E Cohen, E Alkassar, V Boyarinov, M Dahlweid, U Degenbaev, ...
Perspectives of Systems Informatics: 7th International Andrei Ershov …, 2010
132010
ProofPeer: Collaborative theorem proving
S Obua, J Fleuriot, P Scott, D Aspinall
arXiv preprint arXiv:1404.6186, 2014
112014
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
92017
Type inference for ZFH
S Obua, J Fleuriot, P Scott, D Aspinall
Intelligent Computer Mathematics: International Conference, CICM 2015 …, 2015
62015
Capturing hiproofs in HOL Light
S Obua, M Adams, D Aspinall
Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and …, 2013
62013
Proofpeer-a cloud-based interactive theorem proving system
S Obua
arXiv preprint arXiv:1201.0540, 2012
62012
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
32016
Proof pearl: looping around the orbit
S Obua
International Conference on Theorem Proving in Higher Order Logics, 223-231, 2007
22007
Abstraction Logic: A New Foundation for (Computer) Mathematics
S Obua
arXiv preprint arXiv:2207.05610, 2022
12022
Compiling Purely Functional Structured Programs
P Scott, S Obua, J Fleuriot
arXiv preprint arXiv:1703.05227, 2017
12017
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20