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 | 342 | 2017 |

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 | 154 | 2011 |

Importing hol into isabelle/hol S Obua, S Skalberg International Joint Conference on Automated Reasoning, 298-302, 2006 | 89 | 2006 |

Flyspeck II: the basic linear programs S Obua Technische Universität München, 2008 | 41 | 2008 |

Proving bounds for real linear programs in Isabelle/HOL S Obua International Conference on Theorem Proving in Higher Order Logics, 227-244, 2005 | 33 | 2005 |

Partizan games in Isabelle/HOLZF S Obua International Colloquium on Theoretical Aspects of Computing, 272-286, 2006 | 23 | 2006 |

Checking conservativity of overloaded definitions in higher-order logic S Obua International Conference on Rewriting Techniques and Applications, 212-226, 2006 | 19 | 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, ... International Andrei Ershov Memorial Conference on Perspectives of System …, 2009 | 14 | 2009 |

ProofPeer: Collaborative theorem proving S Obua, J Fleuriot, P Scott, D Aspinall arXiv preprint arXiv:1404.6186, 2014 | 11 | 2014 |

Capturing hiproofs in hol light S Obua, M Adams, D Aspinall International Conference on Intelligent Computer Mathematics, 184-199, 2013 | 6 | 2013 |

Proofpeer-a cloud-based interactive theorem proving system S Obua arXiv preprint arXiv:1201.0540, 2012 | 6 | 2012 |

Type inference for ZFH S Obua, J Fleuriot, P Scott, D Aspinall International Conference on Intelligent Computer Mathematics, 87-101, 2015 | 5 | 2015 |

Proofscript: Proof scripting for the masses S Obua, P Scott, J Fleuriot International Colloquium on Theoretical Aspects of Computing, 333-348, 2016 | 3 | 2016 |

Proof pearl: looping around the orbit S Obua International Conference on Theorem Proving in Higher Order Logics, 223-231, 2007 | 2 | 2007 |

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 | 1 | 2017 |

Local Lexing S Obua, P Scott, J Fleuriot arXiv preprint arXiv:1702.03277, 2017 | 1 | 2017 |

Social Network Processes in the Isabelle and Coq Theorem Proving Communities J Fleuriot, S Obua, P Scott arXiv preprint arXiv:1609.07127, 2016 | 1 | 2016 |