# Questions tagged [formalization]

Questions on the computer-formalisation of mathematics, in proof assistants and related software

13
questions

**2**

votes

**4**answers

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

**3**

votes

**0**answers

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

**12**

votes

**4**answers

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

**105**

votes

**5**answers

10k 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

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

**3**

votes

**2**answers

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

**37**

votes

**35**answers

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

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

**2**

votes

**2**answers

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

**0**

votes

**2**answers

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

**59**

votes

**9**answers

6k 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

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

**5**

votes

**3**answers

944 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 ?