The challenge of computer mathematics
From MaRDI portal
Publication:5301849
DOI10.1098/rsta.2005.1650zbMath1152.03304OpenAlexW2140583545WikidataQ33224075 ScholiaQ33224075MaRDI QIDQ5301849
Freek Wiedijk, Hendrik Pieter 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
Symbolic computation and algebraic computation (68W30) Philosophical and critical aspects of logic and foundations (03A05) Mechanization of proofs and logical operations (03B35)
Related Items (11)
The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Programming and Proving with Classical Types ⋮ 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 ⋮ Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker ⋮ Sorting nine inputs requires twenty-five comparisons ⋮ Experimental mathematics, computers and the a priori ⋮ Mathematical knowledge representation: semantic models and formalisms ⋮ Scalable fine-grained proofs for formula processing ⋮ A Vernacular for Coherent Logic ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
Uses Software
Cites Work
- Riemann's hypothesis and tests for primality
- Every planar map is four colorable. I: Discharging
- Every planar map is four colorable. II: Reducibility
- \(\lambda\)-definability and recursiveness
- Hilbert's Tenth Problem is Unsolvable
- How to Write a Proof
- Types for Proofs and Programs
- On Computable Numbers, with an Application to the Entscheidungsproblem
- Type theories, toposes and constructive set theory: Predicative aspects of AST
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The challenge of computer mathematics
