The tag has no wiki summary.

learn more… | top users | synonyms

19
votes
32answers
1k 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
2answers
229 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
2answers
605 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
2answers
394 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
3answers
404 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
3answers
655 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 ?