# Questions tagged [computer-assisted-proofs]

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

57 questions
Filter by
Sorted by
Tagged with
470 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 ...
• 993
16 views

### Help with sample size for finding average distance betwee geographical points

I have a program that I want to test through simulations (since I don't know exactly how it works). The program converts a precise location (lat, lon) to an approximate location (it adds noise and ...
43 views

### Example for a mathematical theorem that has been verified via computer up to very large numbers yet turned out to be false [duplicate]

I am looking for an: Example of a mathematical theorem that has been verified via computer up to very large numbers yet turned out to be false Any suggestions?
126 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: ...
• 5,627
194 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: ...
• 169
166 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 ...
718 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,483
110 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 ...
• 315
2k 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 ...
118 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
257 views

• 1,331
5k 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.
• 8,302
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,859
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 ...