| A formal proof of the Kepler conjecture T Hales, M Adams, G Bauer, TD Dang, J Harrison, LT Hoang, C Kaliszyk, ... Forum of mathematics, Pi 5, e2, 2017 | 555 | 2017 |
| Proof artifact co-training for theorem proving with language models JM Han, J Rute, Y Wu, EW Ayers, S Polu arXiv preprint arXiv:2102.06203, 2021 | 166 | 2021 |
| Algorithmic randomness, reverse mathematics, and the dominated convergence theorem J Avigad, ET Dean, J Rute Annals of Pure and Applied Logic 163 (12), 1854-1864, 2012 | 43 | 2012 |
| Oscillation and the mean ergodic theorem for uniformly convex Banach spaces J Avigad, J Rute Ergodic theory and dynamical systems 35 (4), 1009-1027, 2015 | 35 | 2015 |
| Magistral A Rastogi, AQ Jiang, A Lo, G Berrada, G Lample, J Rute, J Barmentlo, ... arXiv preprint arXiv:2506.10910, 2025 | 31 | 2025 |
| Metastable convergence theorems J Avigad, E Dean, J Rute arXiv preprint arXiv:1108.4400, 2011 | 30 | 2011 |
| Computable randomness and betting for computable probability spaces J Rute Mathematical Logic Quarterly 62 (4-5), 335-366, 2016 | 25 | 2016 |
| Van Lambalgen’s Theorem for uniformly relative Schnorr and computable randomness K Miyabe, J Rute Proceedings of the 12th Asian Logic Conference, 251-270, 2013 | 24 | 2013 |
| Topics in algorithmic randomness and computable analysis J Rute Carnegie Mellon University, 2013 | 22 | 2013 |
| Algorithmic randomness, martingales, and differentiability I J Rute preprint 18, 25, 2012 | 21 | 2012 |
| Voxtral AH Liu, A Ehrenberg, A Lo, C Denoix, C Barreau, G Lample, JM Delignon, ... arXiv preprint arXiv:2507.13264, 2025 | 18 | 2025 |
| 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 | 16 | 2015 |
| Graph2Tac: Learning hierarchical representations of math concepts in theorem proving J Rute, M Olšák, L Blaauwbroek, FIS Massolo, J Piepenbrock, V Pestun | 13 | 2024 |
| Computable measure theory and algorithmic randomness M Hoyrup, J Rute Handbook of Computability and Complexity in Analysis, 227-270, 2021 | 12 | 2021 |
| Graph2Tac: Online representation learning of formal math concepts L Blaauwbroek, M Olšák, J Rute, FIS Massolo, J Piepenbrock, V Pestun arXiv preprint arXiv:2401.02949, 2024 | 11 | 2024 |
| When does randomness come from randomness? J Rute Theoretical Computer Science 635, 35-50, 2016 | 11 | 2016 |
| 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 | 8 | 2017 |
| Schnorr randomness for noncomputable measures J Rute Information and Computation 258, 50-78, 2018 | 6 | 2018 |
| On the computability of graphons NL Ackerman, J Avigad, CE Freer, DM Roy, JM Rute arXiv preprint arXiv:1801.10387, 2018 | 6 | 2018 |
| On computable representations of exchangeable data NL Ackerman, J Avigad, CE Freer, DM Roy, JM Rute Workshop on Probabilistic Programming Semantics, 2017, 2017 | 5 | 2017 |
Jeremy AvigadProfessor of Philosophy and Mathematical Sciences, Carnegie Mellon UniversityVerified email at cmu.edu
