# Questions tagged [computer-assisted-proofs]

Proofs that are partially or entirely checked by computer, including those formalised in interactive theorem provers.

53 questions
Filter by
Sorted by
Tagged with
77 views

### Lean and inacessible cardinals

Here it is claimed that Lean's type theory is equiconsistent with ZFC + existence of $n$ inacessible cardinals for every natural $n$. This is a bit worrying if you just want to work with pure ZFC: how ...
• 41
140 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 ...
461 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,...
• 4,878
1 vote
101 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 ...
• 313
1k 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 ...
98 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
125 views

• 1,403
4k views

### What are some theorems that currently only have computer-assisted proofs?

What are some theorems that currently only have computer-assisted proofs? For example, there's the four colour theorem. I am very curious about this and would like to generate a list.
• 7,912
2k views

### Numbers as sum of distinct squares

Yesterday Polish Olympiad of Information Science ended, one of the questions was purely mathematical, Squares (PL). In the task, we have defined square ...
• 1,809
118 views

### Understand a Maple output

My goal is to solve for $L$ in $\frac{(2k)!}{2^kk!}{2nL - L^2 \choose 2k} = \sum_{s=0}^k{L \choose s}{n-L \choose s}s!\frac{(2k-2s)!}{2^{k-s}(k-s)!)}{L-s \choose 2k-2s}.$ I tried to use the solve ...
• 169
433 views

### Where can I download the approx 1500 Appel-Haken reducible configurations in the Four-Color-Theorem proof?

Where can I download computer representations of the approximately 1500 Appel-Haken reducible configurations in the Four-Color-Theorem proof? The Wikipedia article (http://en.wikipedia.org/wiki/...
141 views

### Math via Computers

What computer language is best for doing mathematics? That is, which of C or Ruby or whatever would generally be the widest applicable efficient computer language to master for doing mathematics? In ...
• 547
322 views

### Cut-off Subtraction in Coq

I am new to the world of computer assistant proof programs in general, and Coq in particular. As a result, I have sought to prove some elementary results about integers as a way to … At the moment, I ...
• 101