On preserving the computational content of mathematical proofs: toy examples for a formalising strategy

DOI10.1007/978-3-030-80049-9_26OpenAlexW3185513211MaRDI QIDQ2117791

Angeliki Koutsoukou-Argyraki

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-80049-9_26

zbMATH Keywords

proof theorymachine learningIsabelle/HOLproof assistantsformalisationproof mininginteractive theorem proverscomputational content

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items (1)

A computational study of a class of recursive inequalities

Uses Software

• Isabelle/HOL
• Automath
• HOList

Cites Work

• Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators
• Effective asymptotic regularity for one-parameter nonexpansive semigroups
• Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
• Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
• The computational content of classical arithmetic
• Proofs and Computations
• Opinion: The Mechanization of Mathematics
• Effective Rates of Convergence for the Resolvents of Accretive Operators
• PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On preserving the computational content of mathematical proofs: toy examples for a formalising strategy