The Lean theorem prover (system description) L De Moura, S Kong, J Avigad, F Van Doorn, J von Raumer Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015 | 667 | 2015 |

A machine-checked proof of the odd order theorem G Gonthier, A Asperti, J Avigad, Y Bertot, C Cohen, F Garillot, S Le Roux, ... International conference on interactive theorem proving, 163-179, 2013 | 511 | 2013 |

Gödel’s functional (“Dialectica”) interpretation J Avigad, S Feferman Studies in Logic and the Foundations of Mathematics 137, 337-405, 1998 | 341 | 1998 |

*δ*-Complete Decision Procedures for Satisfiability over the RealsS Gao, J Avigad, EM Clarke International Joint Conference on Automated Reasoning, 286-300, 2012 | 229 | 2012 |

A formal system for Euclid’s Elements J Avigad, E Dean, J Mumma The Review of Symbolic Logic 2 (4), 700-768, 2009 | 194 | 2009 |

Formally verified mathematics J Avigad, J Harrison Communications of the ACM 57 (4), 66-75, 2014 | 116 | 2014 |

A metaprogramming framework for formal verification G Ebner, S Ullrich, J Roesch, J Avigad, L de Moura Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017 | 112 | 2017 |

A formally verified proof of the prime number theorem J Avigad, K Donnelly, D Gray, P Raff ACM Transactions on Computational Logic (TOCL) 9 (1), 2-es, 2007 | 112 | 2007 |

Local stability of ergodic averages J Avigad, P Gerhardy, H Towsner Transactions of the American Mathematical Society 362 (1), 261-288, 2010 | 107 | 2010 |

Computability and analysis: the legacy of Alan Turing. J Avigad, V Brattka, R Downey Turing's Legacy, 1-47, 2014 | 102 | 2014 |

Delta-decidability over the reals S Gao, J Avigad, EM Clarke 2012 27th Annual IEEE Symposium on Logic in Computer Science, 305-314, 2012 | 95 | 2012 |

Mathematical method and proof J Avigad Synthese 153, 105-159, 2006 | 94 | 2006 |

Understanding proofs J Avigad Carnegie Mellon University, 2008 | 91 | 2008 |

Number theory and elementary arithmetic J Avigad Philosophia mathematica 11 (3), 257-284, 2003 | 89 | 2003 |

Building a push-button RESOLVE verifier: Progress and challenges M Sitaraman, B Adcock, J Avigad, D Bronish, P Bucci, D Frazier, ... Formal Aspects of Computing 23, 607-626, 2011 | 88 | 2011 |

The epsilon calculus J Avigad, R Zach | 81 | 2002 |

Methodology and metaphysics in the development of Dedekind's theory of ideals J Avigad Carnegie Mellon University, 2006 | 69 | 2006 |

Interpreting classical theories in constructive ones J Avigad The Journal of Symbolic Logic 65 (4), 1785-1812, 2000 | 68 | 2000 |

Formalizing forcing arguments in subsystems of second-order arithmetic J Avigad Annals of Pure and Applied Logic 82 (2), 165-191, 1996 | 61 | 1996 |

Reliability of mathematical inference J Avigad Synthese 198 (8), 7377-7399, 2021 | 55 | 2021 |