# 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 ...
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: ...
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: ...
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,...
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 ...
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

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.
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 ...
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 ...