If $m$ and $n$ are coprime integers, prove that each of these $m+n-2$ fractions: $$\frac{m+n}{m},\frac{2(m+n)}{m},\frac{3(m+n)}{m},...,\frac{(m-1)(m+n)}{m},$$ $$\frac{m+n}{n},\frac …

Hello, Apparently in COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is descr …

In an unrelated thread Sam Nead intrigued me by mentioning a formalized proof of the Jordan curve theorem. I then found that there are at least two, made on two different systems. …

The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$. According to Coq $$ a \mod 0 = 0$$ and Isabelle proves $$ a …

Hello everyone. I am not a mathematician but recently I was thinking about one of Kimberling's questions he posted here: http://faculty.evansville.edu/ck6/integer/index.html , i.e …

For example I have read that is agony to give a complete proof of the Jordan curve theorem. Since all statements are meant to be justified by the postulates, where does the difficu …

In trying to understand homotopy type theory, I stumbled upon the following silly question, which is likely to be trivial for the experts. Let $B=\sqcup_{n\in\Bbb N} BS_n$, which …

Damien Pous announced code for assumption-free proof of False in Coq which means inconsistency in Coq (without using exploits, lol). Damien is critical of "fully certified decisio …

This question is related to (maybe even the same in intent as) Question 1017, but none of the answers seem to address what I'm looking for. There are a lot of resources available …

Is there any web-based course or materials about logic / automatic theorem proving? (I checked MIT's OpenCourseWare and I only found a vaguely related AI course)

I'm looking for a proof assistant in order to write formal proofs about basic facts of set theory, such as: $a\subseteq a$ $(a,b)=(c,d)\leftrightarrow a=c\land b=d$ Natural ded …

I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over arbitrary (semi)ri …

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good. From a computational perspe …

Suppose You ask a question beginning from "Why some structure is..." or "Why some object has property..." and several answers arises. Which criteria do You use to qualify which an …

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 ?