All Questions
Tagged with mathematics applications
4
questions
5
votes
0
answers
1k
views
What's the general idea (intuition) behind Andrej's topos where reals are countable? [closed]
I am very surprised that Andrej Bauer claimed to have found a topos where reals are countable. He said it'll take a month to write down the proof, and I think that's very understandable.
However, I'm ...
- 6,316
14
votes
4
answers
321
views
Algorithms obtained through constructive formalization
Formal proofs in proof systems that avoid the law of the excluded middle and certain other principles can be automatically converted into algorithms.
What useful new algorithms have been produced by ...
- 901
27
votes
8
answers
961
views
Where can I find lists of theorems that have been verified?
I recall many years ago seeing a very large and well-interlinked (by computer) list of verified results starting from base assumptions and leading to all sorts of things that naive me did not expect ...
18
votes
2
answers
401
views
How can I prove facts about floating point calculations?
In computing, there is a standard called IEEE 754. Unlike in mathematics, computers have to fit numbers into a finite amount of space; to do this, they use a format a bit like scientific notation, ...
- 495