The formalisation tag has no usage guidance.

**20**

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

234 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

616 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

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

**4**

votes

**3**answers

411 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

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