The challenge of computer mathematics

DOI10.1098/RSTA.2005.1650MaRDI QIDQ5301849zbMATH OpenOpenAlexWikidataFDO

Authors Freek Wiedijk, Henk Barendregt

Publication date 20 January 2009

Published in Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1098/rsta.2005.1650

zbMATH Keywords

computer mathematicsformalized proofsproof checking

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Mechanization of proofs and logical operations (03B35) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1351869
• scientific article; zbMATH DE number 733797
• Some fundamental issues in computational mathematics
• scientific article; zbMATH DE number 3531310
• scientific article; zbMATH DE number 3264869
• Mysteries of mathematics and computation

Cites work

• \(\lambda\)-definability and recursiveness
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Every planar map is four colorable. I: Discharging
• Every planar map is four colorable. II: Reducibility
• Hilbert's Tenth Problem is Unsolvable
• How to Write a Proof
• scientific article; zbMATH DE number 1273299 (Why is no real title available?)
• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• scientific article; zbMATH DE number 1021588 (Why is no real title available?)
• scientific article; zbMATH DE number 1120551 (Why is no real title available?)
• scientific article; zbMATH DE number 1157649 (Why is no real title available?)
• scientific article; zbMATH DE number 2085169 (Why is no real title available?)
• scientific article; zbMATH DE number 2115087 (Why is no real title available?)
• On Computable Numbers, with an Application to the Entscheidungsproblem
• Proof-assistants using dependent type systems
• Riemann's hypothesis and tests for primality
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• Types for Proofs and Programs

Cited in

(24)

• Homogeneous length functions on groups: intertwined computer and human proofs
• Mathematical knowledge representation: semantic models and formalisms
• Experimental mathematics, computers and the a priori
• Crystal: Integrating structured queries into a tactic language
• Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
• scientific article; zbMATH DE number 1722693 (Why is no real title available?)
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Soft math math soft
• Formalizing size-optimal sorting networks: extracting a certified proof checker
• scientific article; zbMATH DE number 4148033 (Why is no real title available?)
• scientific article; zbMATH DE number 1086642 (Why is no real title available?)
• NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
• Programming and Proving with Classical Types
• New directions in the foundations of mathematics (2002)
• A vernacular for coherent logic
• Computational logic and the social
• Scalable fine-grained proofs for formula processing
• Formal Reasoning Using Distributed Assertions
• Automated deduction
• Accepted proofs: objective truth, or culturally robust?
• Considerations on approaches and metrics in automated theorem generation/finding in geometry
• Computer theorem proving in mathematics
• Mind the gap: a conciliating short proof of strong normalization for minimal propositional logic
• Sorting nine inputs requires twenty-five comparisons

Describes a project that uses

Uses Software

• Automath
• kepler98

This page was built for publication: The challenge of computer mathematics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5301849)