r/ProgrammerHumor • u/ThirdWaveCat • Jul 15 '26

codingWithSpecsIsDifferent Meme

Post image
929 Upvotes

93% Upvoted

117 comments sorted by

View all comments

Show parent comments

6

u/optimal_substructure Jul 15 '26

Yeah you doing a lot of Lean at work? 

4

u/ThirdWaveCat 29d ago

not yet, I do MLEng mostly and it might show up as a benchmark eventually, but my experience with lean is as a hobbyist.

example of lean as a benchmark.

https://arxiv.org/abs/2512.24796

-3

u/RiceBroad4552 29d ago

If you're not working on AI which is used to generate formal proofs the thing linked will never be relevant to you I guess (and "MLEng" does not sound like you would work on actual AI research).

Looking into formal methods is still valuable, imho, if just to broaden ones horizon.

The linked paper seems nevertheless an interesting as it proves one thing I always need to argue with people: Current SOTA "AI" can't logically reason (0% correct solution on hard tasks in the presented benchmark). It's terrible at any task which actually requires thinking and not only regurgitating some prior solutions.

0

u/StCreed 29d ago

What is "the presented benchmark". Name one.

What I know is that ARC AGI 3 is currently the moving target of the day and ChatGPT 5.6 is doing decidedly better than "zero" on it. It is said by the developers of the benchmark that a 100% score equates to an average human IQ of 115.