(Epistemic status: I consider the following quite obvious and self-evident, but decided to post anyways.^[1])

Mathematics is a social activity done by mathematicians.

— Paul Erdős, probably

There've been a few attempts to create mathematical models of math. The examples that come to my mind are Gödelian Numbering (GN) and Logical Induction (LI). Feel free to suggest more in the comments, but I'll use those as my primary reference points. In this post, I want to contrast them with the way human mathematicians do math by noticing a few features of their process, the ones that are hard to describe with the language of math itself. Those features overlap a lot and reinforce each other, so the distinction I make is subjective. There's also probably more of them, those are just what I was able to think of. What unites them is that they make mathematical progress more tractable.

Theorem Selection

The way in which Kurt Gödel proved his incompleteness theorems was by embedding math into the language of a mathematical theory (number theory in that particular case, but the trick can be done with any theory that's expressive enough). But this way of describing mathematics is very eternalistic: it treats math as one monolith. It does not give advice on how to make progress in math. How could we approach it in a systematic way?

Fighting the LEAN compiler

What if we just try to prove all statements we can find proofs for?

Let's do some back-of-the-envelope Fermi estimations. Here's a LEAN proof of the statement "if and if , then " (sorry for JavaScript highlighting):

example (a : ℕ → ℝ) (t : ℝ) (h : TendsTo a t) (c : ℝ) (hc : 0 < c) :
    TendsTo (fun n ↦ c * a n) (c * t) := by
    simp [TendsTo] at *
    intro ε' hε'
    specialize h (ε'/c ) (by exact div_pos hε' hc)


    obtain ⟨B, hB⟩ := h
    use B
    intro N hN
    specialize hB N hN
    /-theorem (abs_c : |c| = c) := by exact?-/


    calc
    |c * a N - c * t| = |c*(a N - t)| := by ring
    _ = |c| * |a N - t| := by exact abs_mul c (a N - t)
    _ = c * |a N - t| := by rw [abs_of_pos hc]
    _ < ε' := by exact (lt_div_iff₀' hc).mp hB

It's 558 bytes long in its current form. I didn't optimize it for shortness, but let's say that if I did we could achieve 100 bytes, or 800 bits. Let's say that we run a search process that just checks every possible bitstring starting from short ones for whether it is a valid LEAN proof. The...

Roman Malov's Shortform

6

Roman Malov's Shortform

6