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

**21**

votes

**32**answers

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

**3**

votes

**2**answers

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

**2**

votes

**2**answers

620 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

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

**46**

votes

**8**answers

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

414 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

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