**1**

vote

**0**answers

152 views

### Complexity of reordering a matrix which consists independent sub matrices

Introduction:
Given a matrix A of a $k$ regular graph G. The matrix A can be divided into 4 sub matrices based on adjacency of vertex $x \in G$.
$A_x$ is the symmetric matrix of the graph $(G-x)$, ...

**22**

votes

**3**answers

846 views

### What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?

Over the years, advances in machine learning has allowed us to communicate and interact, using the same natural language, more and more semantically with computers, e.g. Google, Siri, Watson, etc. On ...

**4**

votes

**1**answer

352 views

### Set-theoretic tautologies

Let us consider unquantifed formulas of a set theory (for example, NBG), more precisely,
the formulas, constructed from variables and the constants $\emptyset, V$ (the empty set
and the class of all ...

**11**

votes

**4**answers

1k views

### Does formalizing math require search and creativity, or is it near-mechanical?

I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...

**18**

votes

**3**answers

1k views

### Function extensionality: does it make a difference? why would one keep it out of the axioms?

Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the ...

**46**

votes

**1**answer

3k views

### Wanted: a “Coq for the working mathematician”

Sorry for a possibly off-topic question -- there are four StackExchange subs each of which could be construed as the proper place for this question, and I've just picked the one I'm most familiar ...

**21**

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

**18**

votes

**2**answers

1k views

### At which level is it currently possible to write formal proofs?

I am wondering whether I should try to have some fun using proof systems. I have never used such a system, but I have some experiences in logic and programming. My question is: At which level of ...

**0**

votes

**1**answer

312 views

### prod and sig in COQ

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 described the fact that ...

**1**

vote

**2**answers

557 views

### How to interpret conflicting formal proofs about “a mod 0 = ? ”

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 \mod = a$$
...

**2**

votes

**0**answers

2k views

### Why should I trust Coq when assumption-free proof of False in Coq exists? [closed]

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 decision procedure ...

**3**

votes

**1**answer

976 views

### Proving inequalities over algebraic structures

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

**23**

votes

**4**answers

4k views

### Why is it so difficult to write complete (computer verifiable) proofs?

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 difficulty lie?

**1**

vote

**2**answers

947 views

### What is a semigroup or, what do I do with that associativity proof?

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 perspective, one can ...

**43**

votes

**9**answers

4k views

### How do they verify a verifier of formalized proofs?

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. This is quite an ...

**5**

votes

**1**answer

999 views

### Is there a known way to formalise notion that certain theorems are essential ones?

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 answer is correct?
...

**5**

votes

**3**answers

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

**6**

votes

**6**answers

3k views

### Is there any proof assistant based on first-order logic?

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 deduction for ...

**27**

votes

**5**answers

3k views

### Proof assistants for mathematics

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 for people who want ...

**11**

votes

**7**answers

2k views

### Intro to automatic theorem proving / logical foundations?

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)