Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with proof-assistants
Search options not deleted
user 1384
A proof assistant is software used for creating and checking formal proofs; examples include Coq and HOL. This tag is not to be used for requesting assistance on finding proofs. General questions about proof assistants can also be asked on the Proof Assistants Stack Exchange site.
156
votes
Accepted
Proofs shown to be wrong after formalization with proof assistant
Since this question was asked in January there have been some developments. I would like to argue that the scenario raised in the question has now actually happened. Indeed, Sébastien Gouëzel, when fo …
- 2,183
54
votes
2
answers
5k
views
Automatically solving olympiad geometry problems
Warning: I am only an amateur in the foundations of mathematics.
My understanding of this Wikipedia page about Tarski's axiomatization of plane geometry (and especially the discussion about decidabil …
- 82.7k
3
votes
1
answer
502
views
Can Tychonoff's theorem be applied to topological spaces generated by program output in ZFC?
I am confused about an issue in set theory.
Tychonoff's theorem says that "an arbitrary product of compact topological spaces is compact". We often talk of an index set $I$ and then for each $n\in I$ …
- 41.4k
33
votes
What makes dependent type theory more suitable than set theory for proof assistants?
I still find it very surprising that this random talk I gave attracts so much attention, especially as not everything I said was very well thought out. I am more than happy to engage with people in di …
- 41.4k
139
votes
28
answers
19k
views
Which mathematical definitions should be formalised in Lean?
The question.
Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?
Examples.
In the current stable version of the Lean Theorem Prover, topological groups h …
- 840
121
votes
Accepted
Extent of “unscientific”, and of wrong, papers in research mathematics
"Are most areas safe, or contaminated?"
Most areas are fine. Probably all important areas are fine. Mathematics is fine. The important stuff is 99.99999% likely to be fine because it has been careful …
- 41.4k
37
votes
1
answer
1k
views
Real manifolds in a theorem prover?
Which of the formal computer proof verification systems (like Lean, Coq, Agda, Idris, Isabelle-HOL, HOL-Light, Mizar etc) have a basic theory of real manifolds? Up to, say, the definition of a smooth …
- 7,800
16
votes
Which mathematical definitions should be formalised in Lean?
I would like to see a formal definition of the Langlands Group of the rational numbers, with a future eye on formalising the statement of the global Langlands reciprocity conjecture rigorously in the …
- 41.4k