# Tagged Questions

**4**

votes

**1**answer

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

**10**

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

**16**

votes

**3**answers

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

**3**

votes

**1**answer

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

**42**

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

**3**answers

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 ?

**6**

votes

**6**answers

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

**22**

votes

**5**answers

2k 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

1k 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)