×

zbMATH — the first resource for mathematics

Obua, Steven

Compute Distance To:
Author ID: obua.steven Recent zbMATH articles by "Obua, Steven"
Published as: Obua, Steven
Documents Indexed: 10 Publications since 2005

Publications by Year

Citations contained in zbMATH

9 Publications have been cited 61 times in 48 Documents Cited by Year
A revision of the proof of the Kepler conjecture. Zbl 1195.52004
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland
14
2010
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland
11
2017
Flyspeck II: The basic linear programs. Zbl 1184.68465
Obua, Steven; Nipkow, Tobias
11
2009
Proving bounds for real linear programs in Isabelle/HOL. Zbl 1152.68531
Obua, Steven
8
2005
Partizan games in Isabelle/HOLZF. Zbl 1168.68543
Obua, Steven
6
2006
Checking conservativity of overloaded definitions in higher-order logic. Zbl 1151.68637
Obua, Steven
5
2006
Type inference for ZFH. Zbl 1417.68191
Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David
3
2015
Proof pearl: Looping around the orbit. Zbl 1144.68363
Obua, Steven
2
2007
Capturing hiproofs in HOL light. Zbl 1390.68583
Obua, Steven; Adams, Mark; Aspinall, David
1
2013
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland
11
2017
Type inference for ZFH. Zbl 1417.68191
Obua, Steven; Fleuriot, Jacques; Scott, Phil; Aspinall, David
3
2015
Capturing hiproofs in HOL light. Zbl 1390.68583
Obua, Steven; Adams, Mark; Aspinall, David
1
2013
A revision of the proof of the Kepler conjecture. Zbl 1195.52004
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland
14
2010
Flyspeck II: The basic linear programs. Zbl 1184.68465
Obua, Steven; Nipkow, Tobias
11
2009
Proof pearl: Looping around the orbit. Zbl 1144.68363
Obua, Steven
2
2007
Partizan games in Isabelle/HOLZF. Zbl 1168.68543
Obua, Steven
6
2006
Checking conservativity of overloaded definitions in higher-order logic. Zbl 1151.68637
Obua, Steven
5
2006
Proving bounds for real linear programs in Isabelle/HOL. Zbl 1152.68531
Obua, Steven
8
2005
all top 5

Cited by 116 Authors

7 Nipkow, Tobias
5 Kaliszyk, Cezary
4 Hales, Thomas Callister
4 Obua, Steven
3 Aransay, Jesús
3 McLaughlin, Sean
3 Pąk, Karol
3 Paulson, Lawrence Charles
2 Divasón, Jose
2 Gonthier, Georges
2 Guan, Yong
2 Kunčar, Ondřej
2 Popescu, Andrei
2 Rubio García, Julio Jesús
2 Shi, Zhiping
2 Solovyev, Alexey
2 Urban, Josef
2 Wenzel, Makarius
2 Zumkeller, Roland
1 Adams, Mark
1 Adams, Mark F.
1 Allamigeon, Xavier
1 Alt, Helmut
1 Asperti, Andrea
1 Ballarin, Clemens
1 Bancerek, Grzegorz
1 Barthe, Gilles
1 Bauer, Gertrud
1 Bertot, Yves
1 Bogoşel, Beniamin
1 Bourne, David P.
1 Brown, Chad Edward
1 Buchin, Kevin
1 Bucur, Dorin
1 Budzyńska, Katarzyna
1 Bulwahn, Lukas
1 Byliński, Czesław
1 Chaplick, Steven
1 Cheong, Otfried
1 Corneli, Joseph
1 Dang, Tat Dat
1 Domínguez, César
1 Elser, Veit
1 Erkök, Levent
1 Fleuriot, Jacques D.
1 Foster, Simon
1 Fragalà, Ilaria
1 Freitas, Leo
1 Fulla, Marlon
1 Gallego, Edisson
1 Ganesalingam, Mohan
1 Gengelbach, Arve
1 Gómez-Ramírez, Danny Arlen de Jesús
1 Gowers, William Timothy
1 Grabowski, Adam
1 Gravel, Simon
1 Grayson, Daniel Richard
1 Grégoire, Benjamin
1 Gunther, Emmanuel
1 Haftmann, Florian
1 Harrison, John
1 Harrison, John R.
1 Harrison, John W.
1 Hoang, Le Truong
1 Holmes, Kathryn
1 Kallus, Yoav
1 Katz, Ricardo David
1 Kindermann, Philipp
1 Knauer, Christian
1 Konev, Boris
1 Köppe, Matthias
1 Korniłowicz, Artur
1 Krauss, Alexander
1 Lakhnech, Yassine
1 Lawrence, John C.
1 Li, Liming
1 Li, Yongdong
1 Lisitsa, Alexei
1 Liu, Zhenke
1 Magron, Victor
1 Matthews, John W.
1 Matuszewski, Roman
1 Naumowicz, Adam
1 Nguyen, Quang Truong
1 Nguyen, Tat Thang
1 Ould Biha, Sidi
1 Pagano, Miguel
1 Paşca, Ioana
1 Pease, Alison
1 Peletier, Mark Adriaan
1 Pleso, Joseph
1 Rabe, Florian
1 Reed, Chris
1 Rivera, Ismael
1 Rute, Jason
1 Sacerdoti Coen, Claudio
1 Sánchez Terraf, Pedro
1 Scott, Phil
1 Stehn, Fabian
1 Ta Thi Hoai An
...and 16 more Authors

Citations by Year