https://mathoverflow.net/questions/43690/whats-a-mathematici...
https://github.com/ityonemo/2b4m
The tradeoff is that it's more verbose, but you don't have to even know the language to properly decode a proof.
as an exercise for the language, I'm playing around with having Claude formalize an online algebra text:
https://github.com/ityonemo/2b4m/tree/main/aata
LMK what you think
You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.
Not saying your niche doesn't have value, but you can get interesting ideas from there.
Aside: To some degree, the claudisms are the point since the PL is written by Claude and intended to be consumed by claude
it might(?) work? but abstractions exist for a reason (mostly...)
Ie entrust the more tedious aspects but be able to follow along and still have references to check if you are curious about thoroughness.
Almost like a tap with a latex renderer at various insertion points?
Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.
I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly.
But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”).
These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking.
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 ∎
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.
-- An element has at most one two-sided inverse.
inverse-unique : ∀ (M : Monoid) (open Reasoning M)
(x y z : type M)
→ y ⋆ x ＝ unit M
→ x ⋆ z ＝ unit M
→ y ＝ z
inverse-unique M x y z leftInverse rightInverse =
begin
y ⟪ sym (unitᵣAt y) ⟫
y ⋆ unit M ⟪ mapᵣ (sym rightInverse) ⟫
y ⋆ (x ⋆ z) ⟪ sym (associativeAt y x z) ⟫
(y ⋆ x) ⋆ z ⟪ mapₗ leftInverse ⟫
unit M ⋆ z ⟪ unitₗAt z ⟫
z
∎
where open Reasoning M
(If you know Agda, I dare you to look carefully at this example!)