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 | 725 | 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 | 527 | 2013 |
Gödel’s functional (“Dialectica”) interpretation J Avigad, S Feferman Studies in Logic and the Foundations of Mathematics 137, 337-405, 1998 | 344 | 1998 |
δ-Complete Decision Procedures for Satisfiability over the Reals S Gao, J Avigad, EM Clarke International Joint Conference on Automated Reasoning, 286-300, 2012 | 235 | 2012 |
A formal system for Euclid’s Elements J Avigad, E Dean, J Mumma The Review of Symbolic Logic 2 (4), 700-768, 2009 | 201 | 2009 |
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 | 120 | 2017 |
Formally verified mathematics J Avigad, J Harrison Communications of the ACM 57 (4), 66-75, 2014 | 118 | 2014 |
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 | 111 | 2007 |
Local stability of ergodic averages J Avigad, P Gerhardy, H Towsner Transactions of the American Mathematical Society 362 (1), 261-288, 2010 | 109 | 2010 |
Computability and analysis: the legacy of Alan Turing. J Avigad, V Brattka, R Downey Turing's Legacy, 1-47, 2014 | 106 | 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 | 97 | 2012 |
Understanding proofs J Avigad Carnegie Mellon University, 2008 | 96 | 2008 |
Mathematical method and proof J Avigad Synthese 153, 105-159, 2006 | 95 | 2006 |
Number theory and elementary arithmetic J Avigad Philosophia mathematica 11 (3), 257-284, 2003 | 92 | 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 | 86 | 2002 |
Methodology and metaphysics in the development of Dedekind's theory of ideals J Avigad Carnegie Mellon University, 2006 | 72 | 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 | 58 | 2021 |