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 | 461 | 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 | 85 | 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 | 40 | 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 | 34 | 2015 |

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 |

Computable randomness and betting for computable probability spaces J Rute Mathematical Logic Quarterly 62 (4-5), 335-366, 2016 | 23 | 2016 |

Topics in algorithmic randomness and computable analysis J Rute Carnegie Mellon University, 2013 | 19 | 2013 |

Metastable convergence theorems J Avigad, E Dean, J Rute arXiv preprint arXiv:1108.4400, 2011 | 18 | 2011 |

Algorithmic randomness, martingales, and differentiability I J Rute preprint, 2012 | 17 | 2012 |

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 |

When does randomness come from randomness? J Rute Theoretical Computer Science 635, 35-50, 2016 | 10 | 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 | 9 | 2017 |

Computable measure theory and algorithmic randomness M Hoyrup, J Rute Handbook of Computability and Complexity in Analysis, 227-270, 2021 | 7 | 2021 |

On the computability of graphons NL Ackerman, J Avigad, CE Freer, DM Roy, JM Rute arXiv preprint arXiv:1801.10387, 2018 | 5 | 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 |

Algorithmic randomness for Doob's martingale convergence theorem in continuous time B Kjos-Hanssen, PKLV Nguyen, J Rute Logical Methods in Computer Science 10, 2014 | 5 | 2014 |

Graph2Tac: learning hierarchical representations of math concepts in theorem proving J Rute, M Olšák, L Blaauwbroek, FIS Massolo, J Piepenbrock, V Pestun arXiv preprint arXiv:2401.02949, 2024 | 4 | 2024 |

Algorithmic randomness and constructive/computable measure theory J Rute Algorithmic Randomness: Progress and Prospects 50, 58, 2020 | 4 | 2020 |

Algorithmic barriers to representing conditional independence NL Ackerman, J Avigad, CE Freer, DM Roy, JM Rute 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2019 | 4 | 2019 |

Schnorr randomness for noncomputable measures J Rute Information and Computation 258, 50-78, 2018 | 4 | 2018 |