# Questions tagged [proof-assistants]

A proof assistant is software used for creating and checking formal proofs; examples include Coq and HOL. This tag is not to be used for requesting assistance on finding proofs.

52
questions

**6**

votes

**0**answers

284 views

### Proof of Tennenbaum's Theorem by McCarty

Tennenbaum's Theorem in its usual form states that for any countable non-standard model $M$ of PA there is no way to code the elements of $M$ as natural numbers such that either the addition or ...

**3**

votes

**1**answer

298 views

### Can Tychonoff's theorem be applied to topological spaces generated by program output in ZFC?

I am confused about an issue in set theory.
Tychonoff's theorem says that "an arbitrary product of compact topological spaces is compact". We often talk of an index set $I$ and then for each ...

**28**

votes

**4**answers

3k views

### What is the endgoal of formalising mathematics?

Recently, I've become interested in proof assistants such as Lean, Coq, Isabelle, and the drive from many mathematicians (Kevin Buzzard, Tom Hales, Metamath, etc) to formalise all of mathematics in ...

**114**

votes

**5**answers

19k views

### What makes dependent type theory more suitable than set theory for proof assistants?

In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he ...

**5**

votes

**1**answer

130 views

### Information density of proofs?

I am a CS person so please excuse the hand-waving.
Given a set of machine-represented proofs, each different (but not necessarily proving a different thing), what sort of information-theoretic ...

**10**

votes

**2**answers

601 views

### Gödel's ontological proof & Benzmüller's work

For a decade or so, Christoph Benzmüller from Berlin has explored Gödel's ontological proof (and variants) of existence of God. He uses the proof assistant Isabelle/HOL. He recently posted a preprint, ...

**2**

votes

**1**answer

561 views

### Data abstraction in set theory via Urelements

I am working in a setting of set theory where set theory is embedded in simply-typed higher-order logic, basically as described for example in
Chad E. Brown and Cezary Kaliszyk and Karol Pak (2019) ...

**-4**

votes

**1**answer

291 views

### PCP theorem to check hard proofs [closed]

Is it technically possible to check formidable proofs like Mochizuki's using PCP theorem before mathematicians spend time in understanding the mechanics of the proof? If so why have mathematicians not ...

**96**

votes

**2**answers

8k views

### Extent of “unscientific”, and of wrong, papers in research mathematics

This question is cross-posted from academia.stackexchange.com where it got closed with the advice of posting it on MO.
Kevin Buzzard's slides (PDF version) at a recent conference have really ...

**0**

votes

**0**answers

351 views

### Artificial intelligence simulating mathematicians (what a distopia!)

This is kind of soft and naive question, so feel free to shame on me :)
I start from the fact that, in my opinion, what humans are interested in about mathematics are things that we find deep and ...

**12**

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

**43**

votes

**2**answers

3k views

### Automatically solving olympiad geometry problems

Warning: I am only an amateur in the foundations of mathematics.
My understanding of this Wikipedia page about Tarski's axiomatization of plane geometry (and especially the discussion about ...

**33**

votes

**1**answer

1k views

### Real manifolds in a theorem prover?

Which of the formal computer proof verification systems (like Lean, Coq, Agda, Idris, Isabelle-HOL, HOL-Light, Mizar etc) have a basic theory of real manifolds? Up to, say, the definition of a smooth ...

**6**

votes

**3**answers

2k views

### The Lucas argument vs the theorem-provers — who wins and why?

In his paper, "Minds, Machines and Gödel", J.R. Lucas writes the following:
Gödel's theorem [First Incompleteness Theorem, that is—my comment] must apply to cybernetic machines, because it is of ...

**2**

votes

**4**answers

977 views

### A complete formalization of EGA in Lean

I have been lately thinking about the feasibility of creating a "mediocre algebraic geometer" AI. I thought that to train it, one could feed it some large chunks of algebraic geometry presented in an ...

**45**

votes

**2**answers

3k views

### On proof-verification using Coq

So i recently learnt that there is now a certain software called ''Coq'' by which one can check the validity of mathematical proofs. My questions are:
Are there limitations on the kinds of proofs ...

**125**

votes

**28**answers

14k views

### Which mathematical definitions should be formalised in Lean?

The question.
Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?
Examples.
In the current stable version of the Lean Theorem Prover, topological groups ...

**8**

votes

**1**answer

215 views

### Creativity and the mechanization of elementary geometry

In plane geometry, it is customary to say that checking proofs
is a mechanical process but that finding new theorems
is a creative activity.
Citing J. Hadamard, "logic only sanctions the conquests of ...

**8**

votes

**1**answer

306 views

### Automated geometry theorem provers

What is the state of the art concerning automated geometry theorem provers (AGTP)?
I can see that a few computer algebra softwares and dynamic geometry softwares (e.g. geogebra) have embedded provers ...

**30**

votes

**1**answer

550 views

### Proof assistant for working in weaker foundations?

In some of my works I need to prove some results within the internal logic of categories with not much structures (like pretoposes or even just categories with finite limits). The kind of things I ...

**19**

votes

**1**answer

719 views

### Proof assistant, Cura te ipsum

By a bona fide bug in a proof assistant I mean a software flaw which is serious enough to create a possibility of "proving" something which is actually false. This is not a purely ...

**138**

votes

**6**answers

13k views

### Proofs shown to be wrong after formalization with proof assistant

Are there examples of originally widely accepted proofs that were later discovered to be wrong by attempting to formalize them using a proof assistant (e.g. Coq, Agda, Lean, Isabelle, HOL, Metamath, ...

**37**

votes

**4**answers

2k views

### Is there research on human-oriented theorem proving?

I know there is already a research community that is working on automatic theorem proving mostly using logic (and things like Coq and ACL2). However, I came across a lecture from a fields medalist W.T....

**5**

votes

**0**answers

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

**6**

votes

**1**answer

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

**14**

votes

**1**answer

2k views

### Axioms of Choice in constructive mathematics

There is a widely accepted opinion that the Axiom of Countable Choice (further, ACC)
$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \...

**25**

votes

**0**answers

796 views

### Where to submit this work with several unusual features?

I appreciate that questions about where to submit are generally considered off-topic, but I hope that the unusual features of the present case may make it acceptable.
I have put a monograph on github ...

**35**

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

**12**

votes

**3**answers

2k views

### Is there research on Machine Learning techniques to discover conjectures (theorems) in a wide range of mathematics beyond mathematical logic?

Although there already exists active research area, so-called, automated theorem proving, mostly work on logic and elementary geometry.
Rather than only logic and elementary geometry, are there ...

**13**

votes

**3**answers

1k views

### Algorithmic complexity of formal proof verification?

In this question, suppose $S$ is some popular real-world automated proof system that is stronger than or equivalent to Peano Arithmetic. I would be happy with a positive answer to the following for ...

**3**

votes

**1**answer

58 views

### Determine a sign of the limitation of a certain integral

I can't determine a sign of an integral written below and it has hit a dead end.
My setting is rather special.
Let $a\in(0,1)$ be a given constant and $(x_{\varepsilon},y_{\varepsilon})\in[0,a)\times[...

**1**

vote

**0**answers

187 views

### Complexity of reordering a matrix which consists independent sub matrices

Introduction:
Given a matrix A of a $k$ regular graph G. The matrix A can be divided into 4 sub matrices based on adjacency of vertex $x \in G$.
$A_x$ is the symmetric matrix of the graph $(G-x)$, ...

**23**

votes

**3**answers

1k views

### What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?

Over the years, advances in machine learning has allowed us to communicate and interact, using the same natural language, more and more semantically with computers, e.g. Google, Siri, Watson, etc. On ...

**4**

votes

**1**answer

692 views

### Set-theoretic tautologies

Let us consider unquantifed formulas of a set theory (for example, NBG), more precisely,
the formulas, constructed from variables and the constants $\emptyset, V$ (the empty set
and the class of all ...

**15**

votes

**4**answers

1k views

### Does formalizing math require search and creativity, or is it near-mechanical?

I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...

**49**

votes

**3**answers

5k views

### Function extensionality: does it make a difference? why would one keep it out of the axioms?

Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the ...

**76**

votes

**4**answers

6k views

### Wanted: a “Coq for the working mathematician”

Sorry for a possibly off-topic question -- there are four StackExchange subs each of which could be construed as the proper place for this question, and I've just picked the one I'm most familiar with....

**39**

votes

**35**answers

5k views

### Formalizations of category theory in proof assistants

What are the existing formalizations of category theory in proof assistants?
I'm primarily interested in public-domain code implementing category theory in a proof assistant (Coq, Agda, Isabelle/HOL, ...

**21**

votes

**2**answers

3k views

### At which level is it currently possible to write formal proofs?

I am wondering whether I should try to have some fun using proof systems. I have never used such a system, but I have some experiences in logic and programming. My question is: At which level of ...

**0**

votes

**1**answer

489 views

### prod and sig in COQ

Hello,
Apparently in COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that ...

**2**

votes

**2**answers

810 views

### How to interpret conflicting formal proofs about “a mod 0 = ? ”

The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$.
According to Coq
$$ a \mod 0 = 0$$
and Isabelle proves
$$ a \mod = a$$
...

**4**

votes

**0**answers

3k views

### Why should I trust Coq when assumption-free proof of False in Coq exists? [closed]

Damien Pous announced code for assumption-free proof of False in Coq which means inconsistency in Coq (without using exploits, lol).
Damien is critical of "fully certified decision procedure ...

**47**

votes

**7**answers

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

**3**

votes

**1**answer

1k views

### Proving inequalities over algebraic structures

I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over ...

**29**

votes

**4**answers

4k views

### Why is it so difficult to write complete (computer verifiable) proofs?

For example I have read that is agony to give a complete proof of the Jordan curve theorem. Since all statements are meant to be justified by the postulates, where does the difficulty lie?

**2**

votes

**2**answers

1k views

### What is a semigroup or, what do I do with that associativity proof?

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good.
From a computational perspective, one can ...

**56**

votes

**9**answers

7k views

### How do they verify a verifier of formalized proofs?

In an unrelated thread Sam Nead intrigued me by mentioning a formalized proof of the Jordan curve theorem. I then found that there are at least two, made on two different systems. This is quite an ...

**7**

votes

**1**answer

1k views

### Is there a known way to formalise notion that certain theorems are essential ones?

Suppose You ask a question beginning from "Why some structure is..." or "Why some object has property..." and several
answers arises. Which criteria do You
use to qualify which answer is correct?
For ...

**5**

votes

**3**answers

1k views

### Proof formalization

I read some time ago some papers about proof formalization. Typically, I began whith this one, from Lamport.
Are there more recent works in this field ?

**12**

votes

**7**answers

6k views

### Is there any proof assistant based on first-order logic?

I'm looking for a proof assistant in order to write formal proofs about basic facts of set theory, such as:
$a\subseteq a$
$(a,b)=(c,d)\leftrightarrow a=c\land b=d$
Natural deduction for first-order ...