arXiv:0805.2438cs.LO
Certified Exact Transcendental Real Number Computation in Coq
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
Abstract
Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exact real number computation. I have implemented a library for reasoning and computing with complete metric spaces in the Coq proof assistant and used this library to build a constructive real number implementation including elementary real number functions and proofs of correctness. Using this library, I have created a tactic that automatically proves strict inequalities over closed elementary real number expressions by computation.
He hates Dedekind cuts, not real numbers. Real numbers exist all right, here are some: https://arxiv.org/abs/0805.2438
aeneasmackenzieView on HNParent context