<blockquote>
<p>I feel math is unreal.</p>
</blockquote>
<p>Well, some of it is definitely imaginary. :)</p>
<blockquote>
<p>I wonder if there are any theories about how to use computers to process mathematical proofs ?</p>
</blockquote>
<p>Just a few days ago, Terrence Tao <a href="https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/" rel="nofollow noreferrer">formalized</a> <a href="https://arxiv.org/abs/2311.05762" rel="nofollow noreferrer">his recent work on proving the Freiman--Ruzsa conjecture</a> with W. T. Gowers, Ben Green, Freddie Manners using <a href="https://leanprover-community.github.io/" rel="nofollow noreferrer">Lean</a> (the blue entity <a href="https://x.com/wtgowers/status/1731958963401380146?s=20" rel="nofollow noreferrer"><em>was</em></a> the only remaining theorem not formalized).</p>
<p><a href="https://i.sstatic.net/mVN13.jpg" rel="nofollow noreferrer"><img src="https://i.sstatic.net/mVN13.jpg" alt="enter image description here" /></a></p>
<p>There are other proof assistants (e.g., Coq and Agda)--and a <a href="https://proofassistants.stackexchange.com/">dedicated</a> stack exchange network. <a href="https://blog.computationalcomplexity.org/2023/12/do-we-need-to-formalize.html" rel="nofollow noreferrer">But, Do We Need to Formalize?</a></p>
<p>There also some classic results, for example:</p>
<ul>
<li>The <a href="https://plato.stanford.edu/entries/turing-machine/#HaltProbEnts" rel="nofollow noreferrer">impossibility</a> of the <a href="https://en.wikipedia.org/wiki/Entscheidungsproblem" rel="nofollow noreferrer">Entscheidungsproblem</a> for first-order logic;</li>
<li><a href="https://plato.stanford.edu/entries/hilbert-program/" rel="nofollow noreferrer">Hilbert's program</a> (and particularly <a href="https://plato.stanford.edu/entries/hilbert-program/#4" rel="nofollow noreferrer">Gödel’s incompleteness theorems</a>)</li>
<li><a href="https://plato.stanford.edu/entries/computational-complexity/#SigPNeqNP" rel="nofollow noreferrer"><span class="math-container">$n\text{-}\texttt{PROVABILITY}$</span></a></li>
</ul>
<blockquote>
<p>From a bionic point of view, the neural network appears to be successful. But from my actual use, its mathematical reasoning ability is very weak. It's the lack of training data ?</p>
</blockquote>
<p><a href="https://www.reddit.com/r/singularity/comments/122ilav/comment/jdr0ksn/?utm_source=share&amp;utm_medium=web2x&amp;context=3" rel="nofollow noreferrer">Someone</a> suggested that they suffer from <a href="https://en.wikipedia.org/wiki/Dyscalculia" rel="nofollow noreferrer">Dyscalculia</a>. GPT-3 was trained on <a href="https://arxiv.org/abs/2005.14165" rel="nofollow noreferrer">300 billion tokens</a>, so training data size does not seem to be the problem too.</p>
<blockquote>
<p>But human don't need huge amounts of data to learn to reason.</p>
</blockquote>
<p>Maybe we are only good compressors? However, I believe calls for Hume's <a href="https://davidhume.org/texts/t/full" rel="nofollow noreferrer">Treatise on Human Nature</a> and <a href="https://plato.stanford.edu/entries/kant-reason/" rel="nofollow noreferrer">Kant's Account of Reason</a> are needed at this point.</p>

CC BY-SA 4.0
2023-12-08T14:48:48.253Z
Thanks, I really hit a blind spot in my knowledge.  Seemly proof assistants  is a keyword. Is this thing hard to learn?  Or should I start with mathematical logic?
Enhao Lan
CC BY-SA 4.0
2023-12-08T07:22:17.903Z
2023-12-08T07:22:17.903Z
ndrwnaguib
<p>I'm a PhD in math, but I'm not good. I'm familiar with Riemannian geometry, a little partial differential equations, and a little algebraic topology. And  the other undergraduate courses of math (I know or they are easy to learn for me). I feel math is unreal. And I think what I'm studying is meanless. So I've been looking at some physics stuff lately, starting with the Feynman Physics lecture notes, and I feel good.</p>
<p><strong>I wonder if there are any theories about how to use computers to process mathematical proofs ?</strong></p>
<p>From a bionic point of view, the neural network appears to be successful. But from my actual use, its mathematical reasoning ability is very weak. It's the lack of training data ? But human don't need huge amounts of data to learn to reason.</p>
<p>I'm a layman, and my questions are very unspecific, so I don't expect an accurate answer. I just wanted to know how to start. So, all answers are welcome. Thanks.</p>

CC BY-SA 4.0
2023-12-07T18:38:57.077Z
The keywords you might want to look into are "Automated theorem proving", this mostly covers first-order logic, proof search, hammers (name for automated tools for proving), TacticToe for reinforcment neural network learning, they are far from proving/disproving every theorem, not even due to incompletness, so this is a long way off being able to prove all the theorems you might want. Also I would recommend checking out Thibault Gauthier's disseration, Learning-Assisted Reasoning within Proof Assistants.
Ilk
CC BY-SA 4.0
2023-12-08T14:30:46.420Z
@Ilk Thanks, Thibault Gauthier's disseration seemly be interesting.   Hope I can understand it. What pre-knowledge is required for this paper?
Enhao Lan
CC BY-SA 4.0
2023-12-08T21:55:07.843Z
The learning part is outside of my domain, so I cant judge that well. It's useful to have some experience with proving in tactic-based proof assistants.
Ilk
<soft-question><proofs>
If I want to end math, where should I start?
Enhao Lan
# If I want to end math, where should I start?

(Asked by: username_0 on 2023-12-07)

I'm a PhD in math, but I'm not good. I'm familiar with Riemannian geometry, a little partial differential equations, and a little algebraic topology. And the other undergraduate courses of math (I know or they are easy to learn for me). I feel math is unreal. And I think what I'm studying is meanless. So I've been looking at some physics stuff lately, starting with the Feynman Physics lecture notes, and I feel good.

**I wonder if there are any theories about how to use computers to process mathematical proofs ?**

From a bionic point of view, the neural network appears to be successful. But from my actual use, its mathematical reasoning ability is very weak. It's the lack of training data ? But human don't need huge amounts of data to learn to reason.

I'm a layman, and my questions are very unspecific, so I don't expect an accurate answer. I just wanted to know how to start. So, all answers are welcome. Thanks.

**Tags:** soft-question, proofs
> **Comments:**
> **username_1**: The keywords you might want to look into are "Automated theorem proving", this mostly covers first-order logic, proof search, hammers (name for automated tools for proving), TacticToe for reinforcment neural network learning, they are far from proving/disproving every theorem, not even due to incompletness, so this is a long way off being able to prove all the theorems you might want. Also I would recommend checking out Thibault Gauthier's disseration, Learning-Assisted Reasoning within Proof Assistants.  
> **username_0**: @Ilk Thanks, Thibault Gauthier's disseration seemly be interesting.   Hope I can understand it. What pre-knowledge is required for this paper?  
> **username_1**: The learning part is outside of my domain, so I cant judge that well. It's useful to have some experience with proving in tactic-based proof assistants.  

---

## 1 answers

### Answer by username_2 on 2023-12-08. Score: 1 | Accepted answer

> I feel math is unreal.

Well, some of it is definitely imaginary. :)

> I wonder if there are any theories about how to use computers to process mathematical proofs ?

Just a few days ago, Terrence Tao [formalized](https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/) [his recent work on proving the Freiman--Ruzsa conjecture](https://arxiv.org/abs/2311.05762) with W. T. Gowers, Ben Green, Freddie Manners using [Lean](https://leanprover-community.github.io/) (the blue entity [*was*](https://x.com/wtgowers/status/1731958963401380146?s=20) the only remaining theorem not formalized).

[![enter image description here](https://i.sstatic.net/mVN13.jpg)](https://i.sstatic.net/mVN13.jpg)

There are other proof assistants (e.g., Coq and Agda)--and a [dedicated](https://proofassistants.stackexchange.com/) stack exchange network. [But, Do We Need to Formalize?](https://blog.computationalcomplexity.org/2023/12/do-we-need-to-formalize.html)

There also some classic results, for example:

* The [impossibility](https://plato.stanford.edu/entries/turing-machine/#HaltProbEnts) of the [Entscheidungsproblem](https://en.wikipedia.org/wiki/Entscheidungsproblem) for first-order logic;
* [Hilbert's program](https://plato.stanford.edu/entries/hilbert-program/) (and particularly [Gödel’s incompleteness theorems](https://plato.stanford.edu/entries/hilbert-program/#4))
* [$n\text{-}\texttt{PROVABILITY}$](https://plato.stanford.edu/entries/computational-complexity/#SigPNeqNP)

> From a bionic point of view, the neural network appears to be successful. But from my actual use, its mathematical reasoning ability is very weak. It's the lack of training data ?

[Someone](https://www.reddit.com/r/singularity/comments/122ilav/comment/jdr0ksn/?utm_source=share&utm_medium=web2x&context=3) suggested that they suffer from [Dyscalculia](https://en.wikipedia.org/wiki/Dyscalculia). GPT-3 was trained on [300 billion tokens](https://arxiv.org/abs/2005.14165), so training data size does not seem to be the problem too.

> But human don't need huge amounts of data to learn to reason.

Maybe we are only good compressors? However, I believe calls for Hume's [Treatise on Human Nature](https://davidhume.org/texts/t/full) and [Kant's Account of Reason](https://plato.stanford.edu/entries/kant-reason/) are needed at this point.

> **Comments:**
> **username_0**: Thanks, I really hit a blind spot in my knowledge.  Seemly proof assistants  is a keyword. Is this thing hard to learn?  Or should I start with mathematical logic?  

---

