| 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 | 794 | 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 | 538 | 2013 |
| Gödel’s functional (“Dialectica”) interpretation J Avigad, S Feferman Studies in Logic and the Foundations of Mathematics 137, 337-405, 1998 | 346 | 1998 |
| δ-Complete Decision Procedures for Satisfiability over the Reals S Gao, J Avigad, EM Clarke International Joint Conference on Automated Reasoning, 286-300, 2012 | 239 | 2012 |
| A formal system for Euclid’s Elements J Avigad, E Dean, J Mumma The Review of Symbolic Logic 2 (4), 700-768, 2009 | 206 | 2009 |
| Formally verified mathematics J Avigad, J Harrison Communications of the ACM 57 (4), 66-75, 2014 | 127 | 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 | 124 | 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 | 116 | 2007 |
| Computability and analysis: the legacy of Alan Turing. J Avigad, V Brattka, R Downey Turing's Legacy, 1-47, 2014 | 114 | 2014 |
| Local stability of ergodic averages J Avigad, P Gerhardy, H Towsner Transactions of the American Mathematical Society 362 (1), 261-288, 2010 | 113 | 2010 |
| Delta-decidability over the reals S Gao, J Avigad, EM Clarke 2012 27th Annual IEEE Symposium on Logic in Computer Science, 305-314, 2012 | 99 | 2012 |
| Understanding proofs J Avigad Carnegie Mellon University, 2008 | 99 | 2008 |
| Mathematical method and proof J Avigad Synthese 153, 105-159, 2006 | 96 | 2006 |
| Number theory and elementary arithmetic J Avigad Philosophia mathematica 11 (3), 257-284, 2003 | 93 | 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 | 88 | 2002 |
| Methodology and metaphysics in the development of Dedekind's theory of ideals J Avigad Carnegie Mellon University, 2006 | 73 | 2006 |
| Interpreting classical theories in constructive ones J Avigad The Journal of Symbolic Logic 65 (4), 1785-1812, 2000 | 69 | 2000 |
| Theorem proving in Lean J Avigad, L De Moura, S Kong Carnegie Mellon University, 2021 | 65 | 2021 |
| Reliability of mathematical inference J Avigad Synthese 198 (8), 7377-7399, 2021 | 63 | 2021 |
Leonardo de MouraAmazon Web ServicesEmail verificata su amazon.com
