Skip to main content

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. General questions about proof assistants can also be asked on the Proof Assistants Stack Exchange site.

Filter by
Sorted by
Tagged with
23 votes
1 answer
2k views

What is known about the theory of natural numbers with only 0, successor and max?

Consider the first-order theory whose intended/standard model is the natural numbers $\mathbb{N}$, with constant $0\in \mathbb{N}$, with an injective successor operation $s$ such that $0$ is not a ...
David Roberts's user avatar
  • 34.8k
14 votes
0 answers
686 views

Explicit and complete list of Lean's Axioms

I'm a big fan of the idea of fully formalizing mathematics. So the Lean proof checker appeals to me. Relating to this, one of the biggest appeals of mathematics to me is that there is a (largely) ...
Luke Elliott's user avatar
0 votes
1 answer
399 views

How bad is Coq proving both $T$ and $\lnot T$? [closed]

Question: How bad is Coq proving both $T$ and $\lnot T$? Can it be abused? Back in 2011 on the coq-club mailing list there was a thread: Is the Daniel Schepler's inconsistency real?. In the thread ...
joro's user avatar
  • 24.7k
7 votes
1 answer
231 views

Formulas that are valid simultaneously in a power set Boolean algebra $B$ and the 2-element Boolean algebra $\mathbf2$ [duplicate]

Note 1. Early I posted a related question Set-theoretic tautologies. But the answer did not contain any concrete references to the literature. So I posted this, more precisely formulated question, ...
Victor Makarov's user avatar
5 votes
0 answers
154 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 ...
Marcos Cramer's user avatar
10 votes
0 answers
331 views

Feferman's universes for proof assistants?

This question was prompted by a discussion from another MO question about the consistency of ZFC. There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them,...
Timothy Chow's user avatar
  • 80.3k
11 votes
3 answers
718 views

Can computers find zeros of order $2$?

We assume we are given an entire function $f: \mathbb C \to \mathbb C$ with $f(0)=1$ and $f'(0)=0$ and $f$ is real on the real axis. We assume (as a fact about $f$, that we want to demonstrate ...
Pritam Bemis's user avatar
9 votes
0 answers
369 views

Locally small categories in ZFC

This question is primarily a reference request. It arose from a personal coding/formalization project. I am using a particular form of a definition of a category in ZFC. According to this definition, ...
user9716869 - supports Ukraine's user avatar
3 votes
0 answers
376 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. ...
Student's user avatar
  • 5,038
8 votes
0 answers
628 views

Theorem proving in Lean, for areas that aren't quite ready for it

While taking a break from being stuck, I have found myself addicted to playing with the Lean Theorem Prover. (Beware, if you visit this link might you might find yourself hooked...) Playing with this ...
Jon Bannon's user avatar
  • 7,037
4 votes
2 answers
553 views

Checking elementary proofs with proof checkers

I am not sure if this is the right place to post this, but I have seen discussions related to proof checking here, so let me post it. If there is better place for it, please give me a hint as to where ...
EGME's user avatar
  • 1,018
0 votes
0 answers
295 views

Can ∞-category be defined in proof assistants?

Can ∞-category be defined in proof assistants? For example, we can directly consider a function such as ...
Hexirp's user avatar
  • 325
72 votes
13 answers
11k views

The use of computers leading to major mathematical advances II

I would like to ask about recent examples, mainly after 2015, where experimentation by computers or other use of computers has led to major mathematical advances. This is a continuation of a question ...
18 votes
1 answer
2k views

Available frameworks for homotopy type theory

I am thinking about trying to formalise some parts of classical unstable homotopy theory in homotopy type theory, especially the EHP and Toda fibrations, and some related work of Gray, Anick and Cohen-...
Neil Strickland's user avatar
6 votes
0 answers
418 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 ...
Léreau's user avatar
  • 211
3 votes
1 answer
492 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 ...
Kevin Buzzard's user avatar
33 votes
4 answers
4k 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 ...
155 votes
5 answers
28k 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 ...
MWB's user avatar
  • 1,647
5 votes
1 answer
218 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 ...
user318904's user avatar
10 votes
2 answers
857 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, ...
Denis Serre's user avatar
  • 51.9k
3 votes
1 answer
668 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) ...
Steven Obua's user avatar
-3 votes
1 answer
472 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 ...
VS.'s user avatar
  • 1,826
99 votes
2 answers
11k 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
431 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 ...
Andrea Marino's user avatar
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: ...
ZhangLiao's user avatar
  • 141
54 votes
2 answers
5k 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 ...
Kevin Buzzard's user avatar
37 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 ...
Kevin Buzzard's user avatar
6 votes
3 answers
3k 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 ...
Thomas Benjamin's user avatar
3 votes
4 answers
2k 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 ...
user avatar
45 votes
2 answers
4k 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 ...
Software enthusiast's user avatar
138 votes
28 answers
18k 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
288 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 ...
coudy's user avatar
  • 18.6k
9 votes
1 answer
349 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 ...
coudy's user avatar
  • 18.6k
33 votes
1 answer
765 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 ...
Simon Henry's user avatar
  • 40.8k
20 votes
1 answer
818 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 ...
Alex Gavrilov's user avatar
152 votes
6 answers
16k 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, ...
38 votes
4 answers
3k 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....
Charlie Parker's user avatar
6 votes
0 answers
295 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 ...
D. Huang's user avatar
  • 161
7 votes
1 answer
749 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 ...
Pedro Sánchez Terraf's user avatar
16 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 . \...
Rubi Shnol's user avatar
26 votes
0 answers
897 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 ...
Neil Strickland's user avatar
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 ...
Dan Piponi's user avatar
  • 8,136
13 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 ...
Xingdong Zuo's user avatar
15 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 ...
Andrew Critch's user avatar
3 votes
1 answer
66 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[...
user's user avatar
  • 201
1 vote
0 answers
204 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)$, ...
Michael's user avatar
  • 267
24 votes
3 answers
2k 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 ...
7 votes
1 answer
1k views

Set-theoretic tautologies

Let us consider unquantified 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 ...
Victor Makarov's user avatar
20 votes
5 answers
2k 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 ...
52 votes
3 answers
7k 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 ...
darij grinberg's user avatar