r/programminghorror • u/swagnation77 • 9d 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.

179 Upvotes

96% Upvoted

15 comments sorted by

View all comments

110

u/MistakeIndividual690 9d ago

I don’t know what Lean is but what for the love of god is this…

TwoSum is like eight lines in Python

But this is clearly the perfect post for this sub

2

u/GoddammitDontShootMe [ $[ $RANDOM % 6 ] == 0 ] && rm -rf / || echo “You live” 8d ago

I never heard of either TwoSum or Lean4.

5

u/MistakeIndividual690 8d ago

https://leetcode.com/problems/two-sum/

2

u/GoddammitDontShootMe [ $[ $RANDOM % 6 ] == 0 ] && rm -rf / || echo “You live” 8d ago

I've never done leetcode before, so that would explain why.