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

learn more… | top users | synonyms (1)

1
vote
0answers
33 views

Generate connected subgraphs as the satisfying assignments to a SAT instance

I want a SAT instance (in CNF) whose set of satisfying assignments are the connected subgraphs of a given input graph. A general solution would be helpful, but I really only need this when the input ...
30
votes
35answers
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, Isabelle/HOL,...
3
votes
2answers
246 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
2answers
632 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
428 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 ...
47
votes
7answers
4k 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
3answers
419 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
751 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 ?