alt Hacker NewsI have a question I'm surprised people are not asking: How did Fable find this? Was it like guessing a bunch of families and then solving for possible solutions in those families? Was it clever search? something else?
Replies
ibarrajo • yesterday at 7:55 AM
I’m doing this by working all logical steps into lean (formal verification) the quick feedback loop between the AI prose and the Lean verification errors and warnings ensures that its logically consistent.
The issue that remains are two things, ensuring the idea of the proof is actually the thing you want to prove and the interpretation of the results you get. But besides that, everything inside of the kernel checked code is logically consistent
➕ show 1 reply
Some speculation in this Claude chat: https://claude.ai/share/22abed98-d9af-43c5-9881-b19e009a07b0
linked from here: https://x.com/b_shrir/status/2079094004885668003?s=20
Very short version: there’s an existing false counterexample in the literature which holds almost everywhere except at a pole. It looks like Fable used this polynomial as a base & extended it in a way that eliminated the pole whilst preserving the structure.