Questions tagged [computer-assisted-proofs]
Proofs that are partially or entirely checked by computer, including those formalised in interactive theorem provers.
57
questions
1
vote
0
answers
74
views
If proofs can be checked by computers, will we ever mistakenly believe a false proof? [closed]
As I understand, math proofs can be formalized and checked by a computer. Does this mean the math community will never have to deal with believing incorrect proofs?
If not, is the issue with adoption ...
4
votes
1
answer
112
views
Computational Complexity of Equational Logic
Equational logic uses a surprisingly small set of axioms to prove all algebraic identities (algebraic in the sense of universal algebra, so things like field theory fall beyond this scope). This makes ...
- 2,346
2
votes
2
answers
501
views
Linear logic proof of $P⊸(Q⊸R)≡(P⊗Q)⊸R$?
I’ve been trying to use https://click-and-collect.linear-logic.org for a while, and have been thinking about exportation/importation for Linear Logic. Intuitively, I thought P⊸(Q⊸R)≡(P⊗Q)⊸R was valid ...
- 1,383
2
votes
0
answers
160
views
Help with Categories in Lean
I'm looking to start a project on categories in Lean. I was wondering if anyone could help me out with finding a few of the basic constructions... maybe you know where to look.
I'd like to be able to:
...
user900250
8
votes
0
answers
266
views
Lean and inaccessible cardinals
Here it is claimed that Lean's type theory is equiconsistent with ZFC + existence of $n$ inaccessible cardinals for every natural $n$. This is a bit worrying if you just want to work with pure ZFC: ...
- 189
3
votes
1
answer
177
views
Why isn't math proofs just a computer trial and error?
I already asked a similar question, but I recently began a course of Logic and it gave me not an answeat but a refination of my question, which I redefine here.
My thinking is the following:
Suppose ...
14
votes
3
answers
808
views
Mathematical logic book that uses a proof assistant?
I'm looking for an introductory book on mathematical logic that also discusses an implementation of its logic in a proof assistant. It seems to me this would be a great way to learn mathematical logic,...
- 6,672
0
votes
1
answer
114
views
Are there integers $a,b,c,d,e,n$ such that $a^3-nb^3=c^3-nd^3=e^3$?
Can anyone help me find (with a computer search) nonzero integers $a,b,c,d,e,n$ such that
$$a^3-nb^3=c^3-nd^3=e^3$$
where $(a,b,e)$ and $(c,d,e)$ are pairwise coprime and $n^2\ne 1$
One solution set ...
- 343
3
votes
2
answers
3k
views
Proof Solver Geometry [closed]
Are there any programs that can solve Geometry Problems?
An example of such a problem would be:
The centroid of a triangle always divides its medians into two sections with a 1:2 ratio.
While that ...
user688736
0
votes
0
answers
128
views
General Idea of HoTT from the use of HoTT Library
I don't have a deep understanding of homotopy type theory, but I'm curious about the difference between coq and HoTT library.
When proving with coq, instead of trying tactics brute force, we roughly ...
1
vote
2
answers
287
views
Prove or disprove the following statement using the definition of big-Θ:
NOTE: I am not provign big O here I am proving big-Θ
Prove or disprove the following statement using the definition of big-Θ:
$$n^2−4n = Θ(2^n)$$
so, by definition, $$T(N)=O(h(N))$$ and $$T(N)=Ω(h(N))$...
- 139
11
votes
1
answer
746
views
Computational Type Theory For Topos Logic
My question is basically, what approaches have been made to make computer proof assistants which can handle the internal logic of a topos ?
To explain: while learning topos theory I was struck by the ...
- 1,659
2
votes
3
answers
80
views
What is the best computational software(free/cheap)? [closed]
I have already tried Wolfram Alpha (not pro) and I don't know whether I can access MATLAB for free, any software than downloaded for free and is easy to use will work. I need it for computing complex ...
- 292
2
votes
1
answer
110
views
Homotopy Type Theory: How long is the computer-assisted proof that concatenation of paths is associative?
My question refers to Lemma $2.1.4\ (\text{iv})$ of the HoTT book. I chose this lemma because it is simple to understand yet tedious to prove by hand. I have never used a proof assistant before, so I'...
- 792
3
votes
1
answer
58
views
Are theorems in a mathematical theory effectively checkable?
I wonder whether it is possible to effectively check whether some theorem of a mathematical theory (for example group theory) is provable from axioms of that theory. I know that in propositional logic ...
- 757