Questions tagged [formal-proof]
The formal-proof tag has no usage guidance.
46 questions
84
votes
3
answers
6k
views
How do I verify the Coq proof of Feit-Thompson?
I probably don't have the appropriate background to even ask this question. I know next to nothing about formal or computer-aided proof, and very little even about group theory. And this question is ...
- 29.7k
62
votes
9
answers
6k
views
Techniques for debugging proofs
After writing many proofs, most of which contained errors in their initial form, I have developed some simple techniques for "debugging" my proofs. Of course, a good way to detect errors in ...
59
votes
8
answers
12k
views
How true are theorems proved by Coq?
Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...
- 35.5k
55
votes
5
answers
6k
views
How much of the ATLAS of finite groups is independently checked and/or computer verified?
In a recent talk Finite groups, yesterday and today Serre made some comments about proofs that rely on the classification of finite simple groups (CFSG) and on the ATLAS of Finite Groups. Namely, he ...
- 35.5k
37
votes
1
answer
4k
views
How much mathematics has been formally verified?
That's a vague question so allow me to tighten it up a bit.
I recently noticed that there is a formal machine verified proof of the Central Limit Theorem (CLT) implemented with Isabelle. This ...
- 8,271
33
votes
0
answers
2k
views
Next steps on formal proof of classification of finite simple groups
While people are steaming ahead on finessing the proof of the classification of finite simple groups (CFSG), we have a formal proof in Coq of one of the first major components: the Feit-Thompson odd-...
- 35.5k
20
votes
1
answer
4k
views
Where can I find Gonthier's Coq code proving the four color theorem?
In a 2008 article in the Notices, Georges Gonthier announced a computer-checked proof of the four color theorem using Coq:
Gonthier, Georges. Formal proof—the four-color theorem.
Notices Amer. ...
- 29.7k
16
votes
3
answers
1k
views
Finite versions of Godel' s incompleteness
Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake ...
- 7,853
14
votes
2
answers
4k
views
Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug? [closed]
Technically, it is possible to prove anything in Coq proof assistant [1] (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis ...
- 25.4k
14
votes
2
answers
1k
views
How does proof assistant organize knowledge?
I am reading a paper
Ittay Weiss, The QED Manifesto after Two Decades — Version 2.0, Journal of Software, 11 no. 8 (2016) pp. 803–815, doi:10.17706/jsw.11.8.803-815
The paper says
Goal 7: ...
- 141
11
votes
2
answers
1k
views
Why is there a need for ordinal analysis?
Consider the Peano axioms. There exists a model for them (namely, the natural numbers with a ordering relation $<$, binary function $+$, and constant term $0$). Therefore, by the model existence ...
- 139
10
votes
2
answers
2k
views
What exactly is a judgement?
Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...
user99916
10
votes
2
answers
452
views
Conjecture on minimum size of graph
Given a graph $G(V,E)$, let $\chi(G)$ be its chromatic number, and $\chi_1(G)$ its 1-improper chromatic number (meaning that each node can have at most 1 neighbor with the same color; or another way ...
- 225
9
votes
4
answers
2k
views
Computational complexity theoretic incompleteness: is that a thing?
Has anyone done research in an area that I have not heard of but that I want to call "Computational complexity theoretic incompleteness", which would mean not absolute incompleteness in the ...
- 193
8
votes
1
answer
455
views
Proving that a combinatorial sequence has no compact formula
Suppose we have a sequence $a_n$ given by some combinatorial formula, e.g. involving a sum of n terms (like ${n \choose k}^{10}3^{-k}$ etc.). Sometimes it is plausible that there is no compact ...
- 3,323
7
votes
1
answer
759
views
Are there any recent advances in formalizing the undecidability of $\mathit{CH}$?
The website Formalizing 100 Theorems by Freek Wiedijk contains a list of some theorems that were chosen at some point as good candidates for formalization (because of their complexity, their ...
- 1,124
6
votes
0
answers
296
views
formalization of coordinate-free linear algebra in a proof assistant
I am aware of projects that formalize linear algebra in existing proof assistants (i.e. Coq), but it seems like most of them are based on matrices. I was wondering if it's done in a coordinate-free ...
- 161
5
votes
4
answers
1k
views
Binomial ID $\sum_{k=m}^p(-1)^{k+m}\binom{k}{m}\binom{n+p+1}{n+k+1}=\binom{n+p-m}{n}$
Could I get some help with proving this identity?
$$\sum_{k=m}^p(-1)^{k+m}\binom{k}{m}\binom{n+p+1}{n+k+1}=\binom{n+p-m}{n}.$$
It has been checked in Matlab for various small $n,m$ and $p$. I have a ...
- 573
5
votes
0
answers
165
views
Formal and informal proofs: Is there any "bilingual corpus"?
There are extensive libraries of formalized mathematics like those of Lean, Coq or Isabelle/HOL. What I am interested in is documents of formalized mathematics that closely follow certain informal ...
- 1,228
4
votes
2
answers
864
views
Uniform Convergence of Moment Generating Function
In the article, "The Empirical Moment Generating Function" by Csörgö, the author defines the empirical moment generating function for a sample of $n$ variables $X_1,X_2, \dots, X_n$ as:
$$
\begin{...
- 141
4
votes
1
answer
259
views
Why we need to choose direction in the "marry the arrows" algorithm?
In the article "Division by three" following algorithm is suggested for building a bijection between sets A and B, given that there's a bijection between {0,1}*A and {0,1}*B. First, we build ...
- 141
4
votes
1
answer
323
views
How to use Meredith’s axiom for classical logic?
I’ve been self-studying axiomatic systems for classical logic for a while. The standard Hilbert/Mendelssohn/Lukasiewicz axiomatizations were a bit tough for me to get used to without using the ...
- 184
4
votes
1
answer
555
views
$\frac {f (0)}{2}+ \sum_{k=1}^{\infty}f (k)=\sum_{n=-\infty}^{\infty} \mathcal{L} \{ f \} (2 \pi i n)$
I obtained the very strange formula above and at begining I was just wanted know how to interpretate it. But now when I know what is this with help of @Carlo Beenakker, I am leaving it as a proof. BTW ...
- 161
4
votes
1
answer
119
views
Proving Equal Set Sizes in Sequential Point Selection on a Real Interval with Variable-Length Intervals
I'm here as an engineer working on a point sampling algorithm and I've noticed that when I perform the algorithm on an ordered set of points in one direction it selects the exact same number of points ...
- 151
3
votes
1
answer
1k
views
Since an inconsistent system can prove its own consistency...
Say a proof for the consistency of a formal system (proved within the formal system) is known. There are two possible cases: 1. the formal system is consistent and it can be and has been proven to be, ...
3
votes
0
answers
227
views
How rigorously can we apply the data supplied by this nonstandard attack on Kuratowski's closure-complement problem?
Suppose a student assigned an advanced version of Kuratowski’s closure-complement problem to solve—one that leaves out the standard hint about the finite upper bound of $14$—decides to look for the ...
- 870
3
votes
0
answers
406
views
Conversion of proofs between HoTT and ZFC
HoTT provides a foundation of math that remains mysterious for
many mathematicians including me. Hence this question.
There are several implementations of math based on ZFC, an
example being MetaMath. ...
- 5,230
2
votes
1
answer
2k
views
Hilbert style axiomatic proof or sequent Calculus?
I am puzzling with the question which of the two proof systems (Hilbert style axiomatic proofs or substructural Sequent Calculi) is the most discriminatory?
With discriminatory I mean is which proof ...
- 305
2
votes
1
answer
121
views
Extending a first-order deductive system with satisfaction relation
I'm trying to structure a proof where there are several algebras instantiated over sets, where the properties that you get from the algebraic theories are important, but the properties of the sets ...
2
votes
1
answer
481
views
Sequent calculus: is there a complete linear reasoning (i.e., no trees)?
In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule.
If no inference rule has ...
- 121
2
votes
0
answers
81
views
Is monotonicity redundant in this definition of Tarskian logics?
Given a logic over a language $L$, which has a consequence relation $\vdash$. This logic is Tarskian if for every $\Gamma \cup \Delta \cup {\alpha} \subseteq L$:
If $\alpha \in \Gamma$, then $\Gamma \...
- 21
2
votes
0
answers
208
views
Are infinite loops possible in the game Prodway?
I'd like to know if infinitely repeating sequences of moves (i.e. cycles) are possible in the following game:
Prodway is a game for two players (Black and White) that is
played on the intersections (...
- 21
2
votes
0
answers
128
views
Go variant: cyclic or not?
I would like to know if a cycle of moves is possible in the Go variant, Savage Go. That is, you capture my stones, I capture your stones, you capture my stones... The game never ends. A position is ...
- 121
2
votes
1
answer
449
views
existence of multiplicity of roots [closed]
Im confuse..I read in an article that in dealing with polynomials, a quadratic equation can have either 2 real roots, 1 equal real root or 2 complex roots...but in dealing with random polynomials only ...
- 123
1
vote
1
answer
1k
views
Where is a proof of "2 is more than 1 plus 1" said by Saunders Mac Lane? [closed]
I came across this statement in the autobiography by Saunders Mac Lane.
It was the interaction between solenoids and group extension that got our collaboration started, and this first work of ...
- 163
1
vote
1
answer
772
views
Is there any danger far from home? (Edited & Revised Version) [closed]
The notion of formal proof is defined by finite sequences ($<\omega$ - sequences) of sentences. In some sense if a sentence $\sigma$ is (finitely) provable from the theory $T$ it is very "near" to ...
user42090
1
vote
1
answer
246
views
Minimal Turing machines associated to math statements
It is known that some famous Number Theoretic problems are equivalent to halting of specific Turing machines:
Goldbach conjecture holds iff a 47 state TM halts
Lagarias' formulation of Riemann ...
- 593
1
vote
0
answers
53
views
Does there exist a database of formalized definitions and theorems based on NBG set heory?
Is there a library of formalized mathematical definitions and theorems similar to Lean's mathlib, but based on Von Neumann–Bernays–Gödel set theory and first order logic, rather than type theory? I am ...
- 11
1
vote
0
answers
171
views
Prove the following property about natural integral
Natural integral is the distinguished antiderivative of a function that can be understood as an analytic continuation of consecutive derivatives of a function towards $-1$th order. It is defined as
$...
- 10.1k
1
vote
0
answers
95
views
Proof -- swapping sum with integral
Problem
In Ceperley's 95 article on path integral Monte Carlo approach I have encountered $\hat{\rho}:L^{2}(R^{3N})\to L^{2}(R^{3N})$
$\hat{\rho} = e^{-\beta \hat{H}}$,
where $\hat{H}$ is a ...
- 11
1
vote
0
answers
1k
views
Are all solutions to an ordinary differential equation continuous solutions to the associated implied differential equation and vice versa?
Now I have to heavily emphasize the fact that I have never studied differential algebra or the concept of other types of differentiation (which is what I believe is the concept behind a differential ...
- 111
1
vote
0
answers
187
views
Expansion of prolate spheroidal harmonics
For two coordinate frames $O'$ and $O''$ both offset along the $z$-axis by $\pm R$ respectively, with corresponding offset spherical coordinates $r'$, $\theta'$, $r''$ and $\theta''$, and with prolate ...
- 573
1
vote
0
answers
259
views
How to prove this Gaussian Mixture theorem? (Fitting/Overfitting)
Note from OP: I gave up and reposted this Question with a Bounty on Cross Validated HERE.
In certain applications, we approximate an unknown pdf by placing uniformly weighted Gaussian terms at each ...
- 111
0
votes
0
answers
70
views
Follow-up question regarding real singular matrices with additional details
After my question whose answer turned out to be false, I re-examined the course of my proof, which is actually seperate from the one in my question, and found out that there's another condition, at ...
- 286
-2
votes
1
answer
192
views
Can we have consistent theories stating opposing provability statements that are non-standardly coded?
I want to coin a notion of "strong provability", to be defined as:
$S$ is strongly provable in $T$ if and only if there is a Gödel code of its proof in $T$ that is strictly smaller than any ...
- 11.3k
-3
votes
1
answer
154
views
Proving that $P($$\{\text{$a$ and $b$ are co-prime}$ }$)=0$ for $a,b$ following the Uniform distribution over $[n, 2n]$ as $n \rightarrow \infty$
I have been working on a problem concerning the "line of sight" from a fixed integer co-ordinate — let's say $(0,0)$ — to a variable co-ordinate $(a,b)$. Having a line of sight means that ...
- 147