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 ...
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,...
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^...
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 ...
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 ...
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 ...
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 ...
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 ?