Writing a New Proof Assistant

Lean is an incredibly awesome programming language, as I’ve mentioned many times before on this blog. It’s blazingly fast, expressive, and has pleasant tooling. I use Lean instead of Python for scripting, I write slides in LeanTeX (I really should try VersoSlides sometime too), and I’ve even made Lean play “Bad Apple!!” at compile time.

But… what if we could use Lean as something more than just a mere programming language, and instead do math in Lean? Maybe prove some theorems like the commutativity of addition and the irrationality of √2?

Well, I’m excited to announce that this dream is now a reality, with InfantLean (officially known as μLean), a DSL for theorem proving embedded inside Lean. InfantLean is so easy to learn that even infants can understand it easily. For example, let’s prove that ¬¬¬A → A!

def not_not_not_a_imp_not_a :=
  (la [’α, ’f, ’a]
    (ap ’f (((’α ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) [
      la [’f] (ap ’f (’α ⇨ ⊥) [’a])
    ]),
    α◆𝒰 ⇨ f◆(((’α ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) ⇨ a◆’α ⇨ ⊥)

You can also use InfantLean as a general-purpose programming language! Here’s a simple and elegant example for the Fibonacci function:

def fib :=
  (la [’n]
    (ar fst [
      ℕ, const ℕ,
      ab nat_rec [
        const nat_pair, ab pmk [ℕ, const ℕ, 0, 1],
        la [’n, ’nf]
          (ab pmk [
            ℕ, const ℕ,
            ar nat_snd [’nf],
            ar fst [ℕ, const ℕ, ’nf] + ar nat_snd [’nf]
          ]),
        ’n
      ]
    ]),
    n◆ℕ ⇨ ℕ)

And here’s a longer proof for the commutativity of addition:

def add_comm :=
  (la [’n, ’m]
    (ab nat_rec [
      la [’m] (’n + ’m =ₙ ’m + ’n),
      □ add_zero_eq_zero_add [’n],
      la [’m, ’h]
        (□ rw [
          ℕ, suc (’m + ’n), suc ’m + ’n,
          la [’x] (suc (’n + ’m) =ₙ ’x),
          □ succ_add [’m, ’n],
          □ rw [
            ℕ, ’n + ’m, ’m + ’n,
            la [’x] (suc (’n + ’m) =ₙ suc ’x),
            ’h, ab refl [ℕ, suc (’n + ’m)]
          ]
        ]),
      ’m
    ]),
    n◆ℕ ⇨ m◆ℕ ⇨ ’n + ’m =ₙ ’m + ’n)

Now some of you are probably asking, does the InfantLean proof assistant have a tactics system? To which I answer, no! Who needs tactics when we have AI, the ultimate tactic? Vibe proving is the future!

OK OK, I’ll stop joking around. Actually, I wrote the type checker, syntactic sugar, and many of the InfantLean proofs by hand, and only used Harmonic’s Aristotle for the most annoyingly tedious proofs like the irrationality of √2. I also found Aristotle to be surprisingly good at debugging my type checker and doesn’t seem to be intimidated by the 200KB AST of a failing proof, unlike me. It also found two soundness bugs in my type checker and I found a third, so don’t put too much trust in InfantLean since obviously I have no idea how to actually write a proof assistant.

Anyways, you can find the code for InfantLean here or here (mirror). Go prove some cool stuff. Do the Natural Number Game in InfantLean. Write an external type checker. Have fun!