Questions tagged [computer-assisted-proofs]

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

Filter by
Sorted by
Tagged with
2 votes
2 answers
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 ...
PW_246's user avatar
  • 993
0 votes
0 answers
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 ...
user2468350's user avatar
0 votes
0 answers
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?
math_undergrad_questions's user avatar
2 votes
0 answers
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: ...
Cayley-Hamilton's user avatar
6 votes
0 answers
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: ...
ZFCarla's user avatar
  • 169
3 votes
1 answer
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 ...
Alexandre Tourinho's user avatar
14 votes
3 answers
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,...
WillG's user avatar
  • 6,483
0 votes
1 answer
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 ...
NumThcurious's user avatar
3 votes
2 answers
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 ...
user avatar
0 votes
0 answers
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 ...
Lageneriq's user avatar
1 vote
2 answers
257 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))$...
bfff's user avatar
  • 139
11 votes
1 answer
624 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 ...
Richard Southwell's user avatar
2 votes
3 answers
76 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 ...
Tim Crosby's user avatar
2 votes
1 answer
106 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'...
simple jack's user avatar
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 ...
TKN's user avatar
  • 757
2 votes
2 answers
170 views

Summing Odd Fractions to One, and Odd Perfect Numbers

The title says it all. Question What exactly is the relationship between Egyptian/unit fractions with odd denominators, and odd perfect numbers? Motivation In a comment underneath the question ...
Jose Arnaldo Bebita Dris's user avatar
3 votes
1 answer
291 views

On the decomposition of $1$ as the sum of Egyptian fractions with odd denominators - Part II

Suppose that we decompose $1$ as a sum of Egyptian fractions with odd denominators. I noticed (from a cursory view) that the fraction $$\frac{1}{3}$$ appears in each of such decompositions. (See: e.g....
Jose Arnaldo Bebita Dris's user avatar
1 vote
1 answer
66 views

On the decomposition of $1$ as the sum of Egyptian fractions with odd denominators

Suppose that we decompose $1$ as a sum of Egyptian fractions with odd denominators. I noticed (from a cursory view) that the fraction $$\frac{1}{3}$$ appears in each of such decompositions. ...
Jose Arnaldo Bebita Dris's user avatar
3 votes
2 answers
3k views

Automatic proof checker

Sorry for the noob question: does it exist an automatic proof checker? I mean, some kind of programming language that validates the steps of a proof. I don't speak of automatic proof finder, just a ...
dami's user avatar
  • 486
67 votes
18 answers
10k views

Unsolved Problems due to Lack of Computational Power

I was recently reading up about computational power and its uses in maths particularly to find counterexamples to conjectures. I was wondering are there any current mathematical problems which we are ...
6 votes
1 answer
454 views

Why typeclasses rather than inductive types to define mathematical structures in Lean?

I am not sure whether this is the right forum for this question, but I am not sure where else to ask (There is no Lean forum afaik). In the Lean Prover mathlib library, typical mathematical ...
user56834's user avatar
  • 12.6k
5 votes
2 answers
426 views

Showcases of formalized mathematics in a system like Coq or Lean?

I have been reading about and trying out type theory based proof assistants Lean and Coq, and I have seen a few formalized proofs of basic, isolated propositions. I am looking for examples, showcases,...
user56834's user avatar
  • 12.6k
0 votes
1 answer
221 views

What language are axioms expressed in?

We can form axioms of Boolean algebra or Set theory by forming some expression like: $a=f(a,b,c,d)$ Which are sort of replacement rules on expression trees. Now people say arithmetic is built on ...
zooby's user avatar
  • 4,331
6 votes
1 answer
542 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 ...
Ram Rachum's user avatar
2 votes
1 answer
63 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 ...
Ryan1729's user avatar
  • 325
0 votes
0 answers
42 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 ...
PyRulez's user avatar
  • 10.1k
3 votes
0 answers
345 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 ...
h3h325's user avatar
  • 396
1 vote
2 answers
231 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 ...
KarmaPeasant's user avatar
0 votes
0 answers
64 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. $\...
georgy_d's user avatar
  • 790
35 votes
8 answers
4k 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 ...
zooby's user avatar
  • 4,331
15 votes
1 answer
681 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 of computers? This is just curiosity more than anything. I was actually wondering ...
Antonio Hernandez Maquivar's user avatar
2 votes
1 answer
414 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 ...
Daniel Donnelly's user avatar
1 vote
1 answer
93 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 ...
Pikaninja's user avatar
2 votes
1 answer
315 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 ...
Antonio Kubiko's user avatar
4 votes
0 answers
160 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 ...
Glu's user avatar
  • 407
0 votes
1 answer
348 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 ...
Leigh Brincat's user avatar
4 votes
2 answers
902 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 ...
Kenny Lau's user avatar
  • 24.9k
7 votes
1 answer
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 ...
tparker's user avatar
  • 5,989
1 vote
1 answer
199 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 ...
TomR's user avatar
  • 1,265
-1 votes
1 answer
69 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?
Jie Fan's user avatar
  • 1,876
25 votes
3 answers
3k 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 ...
JWP_HTX's user avatar
  • 1,614
2 votes
1 answer
4k 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 ...
盛安安's user avatar
  • 165
3 votes
0 answers
100 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. ...
asmeurer's user avatar
  • 9,666
2 votes
1 answer
87 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 ...
user avatar
14 votes
2 answers
2k 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 ...
Jeremy Salwen's user avatar
2 votes
2 answers
154 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}...
Tomas's user avatar
  • 1,331
40 votes
12 answers
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.
Victor's user avatar
  • 8,302
6 votes
1 answer
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 ...
Tacet's user avatar
  • 1,859
0 votes
1 answer
130 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 ...
user160371's user avatar
9 votes
1 answer
493 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/...
Bruy Azca's user avatar