<p>I would suggest you to have a look at modern implementations of open source theorem provers frameworks, such as <a href="https://github.com/leanprover/lean4" rel="nofollow noreferrer">Lean</a> and <a href="https://github.com/coq/coq" rel="nofollow noreferrer">Coq</a>. From there you can have a look into their <a href="https://coq.github.io/doc/master/refman/zebibliography.html" rel="nofollow noreferrer">bibliography</a> to find relevant manuscripts.</p>

CC BY-SA 4.0
2022-07-01T18:20:03.387Z
I recently discovered both lean and coq, and they seem to be what I've been looking for. Thanks :)
mell_o_tron
CC BY-SA 4.0
2022-07-01T21:54:51.590Z
Neither Lean nor Coq are automated theorem provers though, they are interactive proof checkers.  The *Handbook of Satisfiability* by Heule, Kullmann, Wieringa, Biere, is a relatively recent look at modern SAT solvers, the workhorse of all automated theorem provers, including proof automation in interactive systems like Lean.
Martin Berger
CC BY-SA 4.0
2022-07-01T18:16:07.390Z
2022-07-01T18:16:07.390Z
Rexcirus
<p>I'm interested in writing my undergraduate thesis on automated theorem proving, and I've been looking for some material to document myself on the topic.</p>
<p>I was introduced to automated and assisted theorem proving by reading a few books that describe the idea to non-necessarily-technical readers, but they were written between the 1970s and the 80s, and most technical books I am finding on the topic are from that same period. That's not to say that old books are not good, most math books I own are reprints of books from that very period, I'm just wondering whether or not the topic has been of any interest to researchers in the last few years.</p>
<p>If it hasn't, why do you think this is the case? And if it has, what do you think would be a good starting point for me to dive into it?</p>

CC BY-SA 4.0
2022-06-24T17:40:50.983Z
I think the issue is much more of a "too much going on to summarize" than the opposite.

I'm a bit concerned about references to the 70s and 80s, since almost all of the wikipedia references are more recent. https://en.wikipedia.org/wiki/Automated_theorem_proving

How exactly did you search for this?
cody
CC BY-SA 4.0
2022-06-24T17:50:07.060Z
@cody I have been looking for books specifically, I admit I have not looked at the wikipedia references... I'll have a look. As for the "too much going on", do you have any particular suggestion as for what could be a starting point to get to know the subject?
mell_o_tron
CC BY-SA 4.0
2022-06-24T19:06:36.947Z
The Handbook of Automated Reasoning provides a pretty good intro to the research-level issues, but may be too introductory or too advanced depending on your background: https://www.sciencedirect.com/book/9780444508133/handbook-of-automated-reasoning
cody
CC BY-SA 4.0
2022-06-24T19:09:14.503Z
It's a mere 2000 pages, and a bit outdated since it's over 20 years old, but a lot of this still holds up.
cody
CC BY-SA 4.0
2022-06-24T19:17:57.520Z
And it doesn't even *touch* SMT, which is a huge field as well... https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
cody
<automated-theorem-proving>
What's the state of research on automated theorem proving?
mell_o_tron
# What's the state of research on automated theorem proving?

(Asked by: username_0 on 2022-06-24)

I'm interested in writing my undergraduate thesis on automated theorem proving, and I've been looking for some material to document myself on the topic.

I was introduced to automated and assisted theorem proving by reading a few books that describe the idea to non-necessarily-technical readers, but they were written between the 1970s and the 80s, and most technical books I am finding on the topic are from that same period. That's not to say that old books are not good, most math books I own are reprints of books from that very period, I'm just wondering whether or not the topic has been of any interest to researchers in the last few years.

If it hasn't, why do you think this is the case? And if it has, what do you think would be a good starting point for me to dive into it?

**Tags:** automated-theorem-proving
> **Comments:**
> **username_1**: I think the issue is much more of a "too much going on to summarize" than the opposite.  I'm a bit concerned about references to the 70s and 80s, since almost all of the wikipedia references are more recent. https://en.wikipedia.org/wiki/Automated_theorem_proving  How exactly did you search for this?  
> **username_0**: @cody I have been looking for books specifically, I admit I have not looked at the wikipedia references... I'll have a look. As for the "too much going on", do you have any particular suggestion as for what could be a starting point to get to know the subject?  
> **username_1**: The Handbook of Automated Reasoning provides a pretty good intro to the research-level issues, but may be too introductory or too advanced depending on your background: https://www.sciencedirect.com/book/9780444508133/handbook-of-automated-reasoning  
> **username_1**: It's a mere 2000 pages, and a bit outdated since it's over 20 years old, but a lot of this still holds up.  
> **username_1**: And it doesn't even *touch* SMT, which is a huge field as well... https://en.wikipedia.org/wiki/Satisfiability_modulo_theories  

---

## 1 answers

### Answer by username_2 on 2022-07-01. Score: 1 | Accepted answer

I would suggest you to have a look at modern implementations of open source theorem provers frameworks, such as [Lean](https://github.com/leanprover/lean4) and [Coq](https://github.com/coq/coq). From there you can have a look into their [bibliography](https://coq.github.io/doc/master/refman/zebibliography.html) to find relevant manuscripts.

> **Comments:**
> **username_0**: I recently discovered both lean and coq, and they seem to be what I've been looking for. Thanks :)  
> **username_3**: Neither Lean nor Coq are automated theorem provers though, they are interactive proof checkers.  The *Handbook of Satisfiability* by Heule, Kullmann, Wieringa, Biere, is a relatively recent look at modern SAT solvers, the workhorse of all automated theorem provers, including proof automation in interactive systems like Lean.  

---

