Cover Image

Anatomy of a Formal Proof

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Avigad, Jeremy, Commelin, Johan, Macbeth, Heather, Topaz, Adam
Format:	Preprint
Published:	2024
Subjects:	History and Overview Logic in Computer Science 68V20, 68V15, 03B35
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Algorithm and abstraction in formal mathematics
by: Macbeth, Heather
Published: (2024)

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

Formalising New Mathematics in Isabelle: Diagonal Ramsey
by: Paulson, Lawrence C
Published: (2025)

The Network Structure of Mathlib
by: Li, Xinze, et al.
Published: (2026)

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
by: Wang, Zili, et al.
Published: (2025)

Artifical intelligence and inherent mathematical difficulty
by: Dean, Walter, et al.
Published: (2024)

A Higher-Order Vampire (Short Paper)
by: Bhayat, Ahmed, et al.
Published: (2024)

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
by: Farmer, William M.
Published: (2026)

A Modular First Formalisation of Combinatorial Design Theory
by: Edmonds, Chelsea, et al.
Published: (2021)

The extension of zbMATH Open by arXiv preprints
by: Beckenbach, Isabel, et al.
Published: (2024)

A new decision method for Intuitionistic Logic by 3-valued non-deterministic truth-tables (pre-print version)
by: Leme, Renato, et al.
Published: (2023)

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
by: Edmonds, Chelsea, et al.
Published: (2023)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
by: Farmer, William M., et al.
Published: (2023)

The continuous functional calculus in Lean
by: Dedecker, Anatole, et al.
Published: (2025)

Single-set cubical categories and their formalisation with a proof assistant (extended version)
by: Malbos, Philippe, et al.
Published: (2024)

Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization
by: Incatasciato, Guillermo L., et al.
Published: (2024)

Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
by: Lau, Gabriel Rongyang
Published: (2026)

Remote Verification System for Mizar Integrated with Emwiki
by: Kai, Toshiki, et al.
Published: (2024)

A Formalization of Abstract Rewriting in Agda
by: Arkle, Sam, et al.
Published: (2026)

Astrolabe: A Content-Addressable Hypergraph for Semantic Knowledge Management
by: Li, Xinze
Published: (2026)

Formalizing Pick's Theorem, efficiently
by: Eisermann, Michael
Published: (2026)

Universal Algebra in UniMath
by: Amato, Gianluca, et al.
Published: (2021)

Advancing mathematics research with generative AI
by: Carbone, Lisa
Published: (2025)

Universal truth of operator statements via ideal membership
by: Hofstadler, Clemens, et al.
Published: (2022)

Dependent Types Simplified
by: Bice, Tristan
Published: (2025)

Higher-Order Pattern Unification Modulo Similarity Relations
by: Dundua, Besik, et al.
Published: (2025)

Remarks on Primitive Regulation
by: Rosko, Milan
Published: (2026)

A formalization of Borel determinacy in Lean
by: Manthe, Sven
Published: (2025)

Mechanised uniform interpolation for modal logics K, GL, and iSL
by: Férée, Hugo, et al.
Published: (2024)

Internalizing Extensions in Lattices of Type Theories
by: Chan, Jonathan
Published: (2025)

Bounded First-Class Universe Levels in Dependent Type Theory
by: Chan, Jonathan, et al.
Published: (2025)

Formalizing Polynomial Laws and the Universal Divided Power Algebra
by: Chambert-Loir, Antoine, et al.
Published: (2025)

Beyond Eckmann-Hilton: Commutativity in Higher Categories
by: Benjamin, Thibaut, et al.
Published: (2025)

Formalization of Harder-Narasimhan theory
by: Yuan, Yijun
Published: (2025)

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
by: Brossard, Jonathan
Published: (2026)

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
by: Firsching, Moritz, et al.
Published: (2026)

An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
by: Martina, Antoine, et al.
Published: (2023)

Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
by: Zhang, Manqing, et al.
Published: (2026)

Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
by: Edmonds, Chelsea, et al.
Published: (2022)