Untangling mechanized proofs Article Swipe

PDF

Related Concepts

Mathematical proof Scripting language Proof assistant Computer science Programming language Proof of concept Stateful firewall Proof complexity Automated theorem proving Combinatorial proof Interface (matter) Theoretical computer science Discrete mathematics Mathematics Operating system Computer security Network packet Geometry Maximum bubble pressure method Bubble

Clément Pit-Claudel ·

YOU? · · 2020 · Open Access · · DOI: https://doi.org/10.1145/3426425.3426940 · OA: W3106543884

Proof assistants like Coq, Lean, or HOL4 rely heavily on stateful meta-programs called scripts to assemble proofs. Unlike pen-and-paper proofs, proof scripts only describe the steps to take (induct on x, apply a theorem, …), not the states that these steps lead to; as a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive user interface able to run the script and show the corresponding proof states.