I think a lot of people have never actually tried using a proof checker and are forming hot takes based on their imagined assumptions about how they work.
For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):
+-associative : (x y z : Nat) → x + (y + z) ≡ (x + y) + z
+-associative zero y z = refl
+-associative (suc x) y z =
suc x + (y + z) ≡⟨ ap suc (+-associative x y z) ⟩
suc (x + y + z) ≡⟨⟩
(suc x + y) + z ∎
We pattern match on the first nat to get `zero` and `suc x`. In the `zero` case we have `0 + (y + z) = (0 + y) + z`. Both sides compute to `y + z` and thus the equation holds by reflexivity.
In the `suc x` case we need to show that `suc x + (y + z) ≡ (suc x + y) + z`.
`suc x + (y + z)` computes to `suc (x + (y + z))` by the definition of `+`.
By recursively calling `+-associative x y z` we get `x + (y + z) ≡ (x + y) + z`. Then we need to prove that by congruence this is true under `suc`. We get this by passing our proof (from the recursive call to +-associative) into `ap suc`. `ap` says that given `a = b` it is true that `f a = f b`.
Finally, `(suc x + y) + z` computes to `suc ((x + y) + z)`, so the last step holds by computation, which is why it’s just `≡⟨⟩`.
Proof checkers like Lean/Agda/Rocq are literally total functional programming languages with rich type systems.
Everything above comes down to pattern matching and function application. The proof is just a function whose type is the statement we wanted to prove, and the type checker accepting it is what makes it a proof.
This is the Curry-Howard Correspondence in a nutshell. Propositions are types and proofs are programs.
For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):
We pattern match on the first nat to get `zero` and `suc x`. In the `zero` case we have `0 + (y + z) = (0 + y) + z`. Both sides compute to `y + z` and thus the equation holds by reflexivity.In the `suc x` case we need to show that `suc x + (y + z) ≡ (suc x + y) + z`.
`suc x + (y + z)` computes to `suc (x + (y + z))` by the definition of `+`.
By recursively calling `+-associative x y z` we get `x + (y + z) ≡ (x + y) + z`. Then we need to prove that by congruence this is true under `suc`. We get this by passing our proof (from the recursive call to +-associative) into `ap suc`. `ap` says that given `a = b` it is true that `f a = f b`.
Finally, `(suc x + y) + z` computes to `suc ((x + y) + z)`, so the last step holds by computation, which is why it’s just `≡⟨⟩`.
Proof checkers like Lean/Agda/Rocq are literally total functional programming languages with rich type systems.
Everything above comes down to pattern matching and function application. The proof is just a function whose type is the statement we wanted to prove, and the type checker accepting it is what makes it a proof.
This is the Curry-Howard Correspondence in a nutshell. Propositions are types and proofs are programs.