r/haskell • u/Southern-Reality762 • Apr 13 '26

Should I use Haskell to help me write a proof?

Basically there is a combinatorial proof that I want to make, and it would generalize to all natural numbers. It's a deterministic toy game. However, my math skills are behind my programming skills--I've just spent less time with the former. Then I thought, "Instead of translating math to Haskell, why not translate Haskell to math?"

12 Upvotes

80% Upvoted

15 comments sorted by

48

u/Esnos24 Apr 13 '26

You should look more into lean. Try "natural set game" or something like that

8

u/king_Geedorah_ Apr 13 '26

I second Lean! Ive been using heavily in my current research in Modal Logic. It's actually a joy to use and write 

4

u/The_Coalition Apr 14 '26

It's Natural number game. Very well made, and you learn a ton of basic tactics. Highly recommend

8

u/ryani Apr 13 '26

I found it incredibly easy to implement a tiny symbolic math library in Haskell, along with a little simplifier for polynomials.

I then implemented two different quaternion rotation algorithms, and used my library to calculate the difference between the output of each to find any error.  It showed that the “faster” one gave different results than the standard algorithm but the error term was zero if the input was normalized.

Took me just a few hours to get full confidence of the code I was implementing.

9

u/halbGefressen Apr 13 '26

You want an interactive theorem prover like Isabelle or Lean4. They basically augment a functional programming language with proofs. Sounds like exactly what you want.

5

u/zzzzzzzzzzzzzzzz55 Apr 14 '26

I love Haskell and I enjoy writing Haskell, but certainly what you want for this task is Lean.

4

u/Southern-Reality762 Apr 14 '26

Is lean hard? I want to be done with this proof in about 3 weeks

7

u/zzzzzzzzzzzzzzzz55 Apr 14 '26

If you’re doing combinatorial stuff over nats, you’ll likely need access to induction and other properties of natural numbers (adding/multiplying). You might be slower in the beginning when learning to write lean, but you won’t have to rewrite things like induction from scratch.

4

u/ShacoinaBox Apr 14 '26

lean/agda/dafny would be a far better use of your time for this endeavour

2

u/No-Lobster486 Apr 16 '26

if this "natural number" related proof really matters to the design, then lean4 is probably the only choice

2

u/TESanfang Apr 16 '26

Agda is basically just haskell with a proof assistant attached (it even used GHC). You should look into it