I’ve tried (for proofs in English) without much success. It mostly seems to just sort of semi-randomly remove details rather than finding ways to simplify the argument itself, it that makes sense? That doesn’t mean it can’t be made to work! My intuition is that this might work better in Lean, though Goodharting would be a natural concern...
definitely if you train on it. it’s just something measurable to point in a direction or show absolutely no effect. trying to conceive a metric for “good” abstraction is like trying to conceive a metric for beauty. you haven’t quite convinced me that the LLM abstraction isn’t just “human-bad.”
you know working on a worthy problem is like inventing a new language. LLMs might do the same but just have the same translation problems as they do with every other language pair (novel problem language, English or rather the mathematicese dialect thereof).
have you read any reviews of the Lean formalization of Navier-Stokes? I wonder if it is pretty or a tangle.
I’ve tried (for proofs in English) without much success. It mostly seems to just sort of semi-randomly remove details rather than finding ways to simplify the argument itself, it that makes sense? That doesn’t mean it can’t be made to work! My intuition is that this might work better in Lean, though Goodharting would be a natural concern...
definitely if you train on it. it’s just something measurable to point in a direction or show absolutely no effect. trying to conceive a metric for “good” abstraction is like trying to conceive a metric for beauty. you haven’t quite convinced me that the LLM abstraction isn’t just “human-bad.”
you know working on a worthy problem is like inventing a new language. LLMs might do the same but just have the same translation problems as they do with every other language pair (novel problem language, English or rather the mathematicese dialect thereof).
have you read any reviews of the Lean formalization of Navier-Stokes? I wonder if it is pretty or a tangle.
I really have no idea how to judge this: https://github.com/openai/NavierStokesAndEuler/tree/main/NavierStokes
It looks extremely tangled to me, compared to these human-curated proofs. But Navier-Stokes blowup is itself a very complicated thing.
I’d conjecture (just based on my own experience) that it’s possible to make that Navier-Stokes formalization much nicer. But not confident at all.