Questions tagged [computer-assisted-proofs]
Proofs that are partially or entirely checked by computer, including those formalised in interactive theorem provers.
4
votes
1answer
134 views
Is there a theorem prover that works in natural language?
I'm interested in a computer program, possibly a web app, that could prove theorems and show its proofs.
I essentially want to type in a theorem like "For every bounded sequence, there exists a ...
2
votes
1answer
46 views
Have there been any computer proofs that were found to contain bugs post-publication?
I'm curious if there are any known examples of proofs using a computer which after being published, (in a journal or otherwise) turned out to have bugs in the software which invalidated the proof. I'm ...
0
votes
0answers
26 views
Are there any proof assistants based on logic programming?
Logic programming is a programming language paradigm. In it, a programmer creates a bunch of axioms in the form of horn clauses, representing computations, which the implementation of the language ...
1
vote
0answers
85 views
Why weren't Appel and Haken awarded top prizes for proving the Four Color Theorem? [closed]
They may have been over the age limit for the Fields Medal but they weren't awarded the Wolf Prize, Abel Prize or any other award indicative of top-level recognition in mathematics. Is it because they ...
1
vote
0answers
66 views
Strategy for finding trapping region of a discrete Dynamical System (Hénon map)
The Hénon map is defined as $H(x,y) = (f(x,y), g(x,y)$ with $f(x,y) = a - x^2 -by$ and $g(x,y) = x$.
The system is known to have an atractor, I want to find a trapping region for this system. My ...
0
votes
1answer
49 views
Is there little more advanced alternative of “DC Proof”? (it's a proof assistant)
So far I inspected several proof assistant:
1.DC Proof. The closest to my ideal yet still not exactly what I want (although I still have some hope that maybe I'm missing something). I'm glad that it ...
0
votes
0answers
47 views
Subtyping of Prop in Coq. Implementation of Ackermann class theory. First-order theories.
I am trying to implement Ackermann set theory.
The first approach is the code below.
But there is an incorrect axiom "rs_ax".
That's because for every x formula (F x) shouldn't contain predicate M. $\...
29
votes
8answers
3k views
Why is there not a system for computer checking mathematical proofs yet (2018)? [closed]
As of 2018, mathematical proofs are still being decided by human consensus. i.e. Give the proof to a few capable humans and if none of them can find any errors than they vote that the proof is correct ...
11
votes
1answer
184 views
Conjectures Disproven by the use of Computers?
Question: Is there a list of conjectures (famous or not so famous) that were shown to be false by employing the use computers ?
This is just curiosity more than anything. I was actually wondering if ...
2
votes
1answer
171 views
What do you think of this visual category theory tool? See any issues? Would you use it?
The idea behind it is that every category theoretical definition is made with visual diagrams. One reason this is good is that we don't have to do as much language processing which is hard IMO.
Here ...
1
vote
1answer
52 views
Explain how the idea of “partition” is used in the proof of lagrange's theorem? [closed]
I know partiion is a collection of subsets of $S$ that are non empty, disjoint and their union is $S$; and
Lagrange's Theorem: If $G$ is a finite group and $H$ is a subgroup of $G$, then $H$ is a ...
2
votes
1answer
196 views
Can Artificial Intelligence be used to find out reasonable conjectures or even to turn them into theorems by discovering a proof?
Can Artificial Intelligence be used to find out reasonable conjectures or even to turn them into theorems by discovering a proof ? If yes, and after a proof is indeed found through AI, can one ...
4
votes
0answers
108 views
Have there been any (interesting) computer-aided proofs that weren't proof-by-exhaustion?
It seems to me like many of the most famous "computer proofs" were done by basically brute-forcing through all of the cases, such as the four color map theorem. Are there any good examples of computer ...
0
votes
1answer
105 views
Finding a maximum connected planar graph to prove the four colour theorem
Like many, I have been done a lot of reading of the Four Colour Theorem and there is one question that is vexing me to the point where I am sure I am misunderstanding. I hope that someone could help ...
1
vote
0answers
241 views
Is it possible to represent every mathematical (logical) formula as graph and every operation as graph transformation - seeking references and trends? [closed]
In this post I am stating numerous questions that I am asking but I don't expect to receive exhaustive answers here. I am more interested in receiving references, pointers to the literature, "keywords"...
2
votes
2answers
433 views
Meaning of free variables
Consider the statement:
$$\forall x [x=x] \tag1$$
And the statement:
$$x=x \tag2$$
Statement $(1)$ is easily understood: for every $x$ in the universe, $x=x$ is true.
However, what does statement ...
7
votes
1answer
2k views
Which subfields of math are easier or harder to formalize?
This is a follow-up question to Can all math results be formalized and checked by a computer?. Hopefully it's not too broad, but here goes: which subfields of math could be formalized using existing ...
0
votes
1answer
120 views
Is it possible to express Coq Calculus of Constructions in terms of Isabelle/HOL or vice versa?
Is it possible to express Coq Calculus of Constructions in terms of Isabelle/HOL or vice versa? If that could be done then we would be able to import Coq axioms and theorems in Isabelle/HOL. Coq has ...
-1
votes
1answer
64 views
$2^x\equiv 2017\pmod{3^{11}}$ and $2^x\equiv 2016\pmod{11^3}$
Find an integer $x$ such that $2^x\equiv 2017\pmod{3^{11}}$ and $2^x\equiv 2016\pmod{11^3}$
How can I solve this question?
14
votes
2answers
2k views
What is the current state of formalized mathematics?
Russell and Whitehead famously tried to actually create and use a formal system to explicitly develop formal mathematics in their work, "Principia Mathematica."
Much more recently, with the aid of ...
2
votes
1answer
3k views
How do I find an inverse of any element in any group?
I'm working on Agda, which is based on intuitionistic type theory.
I defined groups in Agda with normal laws of groups, which (of course not only) says that there is an inverse element of every ...
2
votes
0answers
80 views
Symbolically formulate the two guard problem so it can be solved by a computer
Take the classic two guard riddle (I don't know where the origin of this riddle is, so I'll take the version from http://www.calpoly.edu/~mcarlton/riddles.html):
You stand at a fork in the road. ...
2
votes
1answer
64 views
Is there any Software package to confirm correctness of your derivation steps?
Suppose I made a very complicated (not necessarily difficult) derivations in which it is very likely for anyone to make some silly mistakes, e.g., incorrect sign, overlooking a term, and so on.
I ...
10
votes
2answers
1k views
Examples of the benefits of Homotopy Type Theory for computer aided proofs?
From what I understand, Homotopy Type Theory is proposed as a new foundation of mathematics, and it supposed to be superior for use with computer aided proofs.
I am currently trying to understand the ...
0
votes
0answers
58 views
$x^4-x \in Z(R)$ implies commutativity [duplicate]
Let $R$ be a ring and $Z(R)$ the centre of $R$. There exist elementary proofs (that is, proofs not using the structure theory of rings) of the fact that if $x^n-x \in Z(R)$, then $R$ is commutative ...
2
votes
2answers
142 views
Are there explicit forms of these integrals
Let $a>0$, and $z_0=r_0e^{i\theta_0}$, where $0<r_0<a$, $0<\theta<\gamma<\frac{\pi}{2}$, do we have a closed form of each of the following integrals
$$
I_1(r_0,\theta_0)=\int_{0}^{a}...
39
votes
12answers
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.
6
votes
1answer
788 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 ...
0
votes
1answer
94 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 ...
8
votes
1answer
212 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/...
0
votes
0answers
63 views
A conjecture on the product of digits of a number
Define $(m,n)$ to be a special pair if $n=m \cdot Pd(n)$. Where $Pd(n)$ is the product of digits $n$.
Then I have the following conjecture -
For every $m$ with no digit of $m$ being $0$ , there ...
7
votes
1answer
122 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 ...
2
votes
0answers
229 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 ...
5
votes
2answers
178 views
What is the meaning of proof of a proof?
After reading about Curry-Howard corrsepondence and looking at some proofs written in coq i've thinked about meaning of proof of a proof.
We can express proofs as a computer program
Proof is correct ...
6
votes
1answer
264 views
Set theory: Metamath Proof of the Pigeon-Hole Principle, Error?
I have recently come to discover Metamath.
Supposedly the language is one that a computer may proof-check.
I then began to look at concepts that I am familiar with, and decided to look up the pigeon ...
6
votes
1answer
92 views
An Auto-Generated Cartography of Mathematical Theories: Has it been done already?
While looking for a way to visualize the logical structure of mathematical theories a graph-like depiction came to my mind, where propositions are represented by vertices. An edge goes from ...
2
votes
1answer
445 views
Online math tool for equation visualisation
I am looking for a math editor that is able to present equations and relations between them. I am not searching for a traditional Latex / MathML editor (I know about various online services that allow ...
3
votes
3answers
276 views
Computer Assisted proofs apart from the 4 color theorem
I recently read about the 4 color theorem and that it was proved using help from computers. Does anybody know of some other 'good' computer-assisted proofs apart from the 4 color theorem?
