Questions tagged [formalization]
Questions on the computer-formalisation of mathematics, in proof assistants and related software
19 questions
6
votes
1
answer
114
views
Filter vs Cover characterization of covering properties
In mathlib, topological properties are generally characterized in terms of filters wherever possible. In particular, a set $K$ is said to be compact provided that ...
- 1,322
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
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
-3
votes
1
answer
319
views
What is a good formalization of this classic math puzzle? [closed]
Here is a classic math olympiad problem (but this is NOT my question!): Each of the girls A and B tells the teacher a positive integer but neither of them knows the other's number. The teacher writes ...
8
votes
0
answers
710
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 ...
- 7,047
5
votes
1
answer
992
views
Does this prove Collatz is a $\Sigma_1$ problem?
So I got an email from one of my colleagues on the Collatz Conjecture with a link to the article Computer Scientists Attempt to Corner the Collatz Conjecture by Kevin Hartnett in Quanta Magazine.
On ...
- 13.9k
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 ...
user141498
3
votes
0
answers
238
views
Research on formalization of what constitutes a good theorem
This question is about automating theorem proving. Now automated theorem proving, as currently understood in CS literature, has little to do with pure mathematics as practiced on this site (I believe ...
user138661
27
votes
5
answers
3k
views
Formalizations of the idea that something is a function of something else?
I'll state my questions upfront and attempt to motivate/explain them afterwards.
Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory?
More ...
- 5,343
157
votes
6
answers
17k
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, ...
0
votes
1
answer
651
views
Literature about most basic existence proofs in graph theory [closed]
I'm writing a MIZAR article about foundations in graph theory e.g. constructing a supergraph from a given graph by adding a vertex to it. The main theorem of the article will be that any graph ...
- 237
4
votes
2
answers
945
views
formalisation of Bourbaki, General Topology
Is there a formalisation of Bourbaki, General Topology book,
particularly its first chapter?
Are there formal proofs of elementary topology arguments such as a Hausdorff compact space is ...
- 113
43
votes
36
answers
6k
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, ...
3
votes
2
answers
270
views
Formalization (and background) of a formula, concering the integral points of a polygon.
I have recently become aware of the following neat statement.
Consider a convex polygon $P$ in the real plane with integral vertices. If we associate with every integral point $(a,b)$ the monomial $x^...
- 3,513
2
votes
2
answers
745
views
All properties of a mathematical object
This is primarily a question about related literature. I am looking for specific references, or terminology that I can use to search for references.
Let A a well defined mathematical structure of ...
- 313
1
vote
2
answers
606
views
Formalization of n-ary functions
Hi there. I've been doing some thinking lately (oh-no!) about function definitions. Specifically, I'm considering functions with multiple parameters.
Now, I'm familiar with "the usual" definition in ...
- 113
59
votes
9
answers
7k
views
Has anyone thought about creating a formal proof wiki with verifier?
Mathematics has undergone some rather nice developments recently with the adoption of new techologies, things like on-line journals, the arXiv, this website, etc. I imagine there must be many further ...
4
votes
3
answers
518
views
reducing a theorem to set theory using first order logic
I'm trying to reduce a simple theorem from number theory (i.e. there are infinitely many primes) to set theory. What do I need to read in order to achieve this? Are there any examples somewhere ?
I ...
- 41
6
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 ?