The formal-proof tag has no usage guidance.

**5**

votes

**0**answers

142 views

### Independence of characters with respect to polynomials

I came across the following property :
Let $\mathfrak{g}$ be a Lie algebra over a ring $k$ without zero divisors,
$\mathcal{U}=\mathcal{U}(\mathfrak{g})$ be its enveloping algebra. As such, $\...

**1**

vote

**0**answers

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

**4**

votes

**0**answers

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

**1**

vote

**0**answers

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

**5**

votes

**0**answers

267 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**

vote

**0**answers

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

**5**

votes

**4**answers

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

**5**

votes

**2**answers

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

**1**

vote

**0**answers

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

**32**

votes

**1**answer

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

**9**

votes

**2**answers

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

**4**

votes

**2**answers

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

**44**

votes

**5**answers

3k views

### How much of the ATLAS of finite groups is independently checked and/or computer verified?

In a recent talk 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 said that a proof that relied on the ...

**26**

votes

**0**answers

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

**2**

votes

**1**answer

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

**70**

votes

**3**answers

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

**14**

votes

**1**answer

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

**0**

votes

**1**answer

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

**2**

votes

**1**answer

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

**1**

vote

**1**answer

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

**1**

vote

**1**answer

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

**2**

votes

**1**answer

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

**16**

votes

**3**answers

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

**8**

votes

**1**answer

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

**13**

votes

**2**answers

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

**42**

votes

**6**answers

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