alt Hacker NewsWhich ones of those have been achieved in your opinion?
I think the arbitrary proofs from mathematical literature is probably the most solved one. Research into IMO problems, and Lean formalization work have been pretty successful.
Then, probably reading a novel and answering questions is the next most successful.
Reliably constructing 10k bug free lines is probably the least successful. AI tends to produce more bugs than human programmers and I have yet to meet a programmer who can reliably produce less than 1 bug per 10k lines.
Replies
kleene_op • yesterday at 11:48 PM
> Reliably constructing 10k bug free lines is probably the least successful.
You imperatively need to try Claude Code, because it absolutely does that.
➕ show 1 reply
Formalizing an arbitrary proof is incredibly hard. For one thing, you need to make sure that you've got at least a correct formal statement for all the prereqs you're relying on, or the whole thing becomes pointless. Many areas of math ouside of the very "cleanest" fields (meaning e.g. algebra, logic, combinatorics etc.) have not seen much success in formalizing existing theory developments.