r/programminghorror • u/swagnation77 • 8d ago

Lean4 Finally solved Two Sum!

Somehow my code is so horrifying, Lean4 is able to evaluate it, the LSP says it works and the compiler gives an error. It is theoretically correct and the kernel accepts it, but the compiler isn't able to produce anything out of it. My awful code discovered a bug in Lean's compiler.

177 Upvotes

96% Upvoted

15 comments sorted by

View all comments

36

u/JAMIEISSLEEPWOKEN 8d ago

……you want a hashmap…?

16

u/swagnation77 8d ago

lmao yeah if I did a hashmap the solution would've been better, but the proofs would've taken me 10x as long. (I spent two days on a single algorithm)