Mickey
4d ago
I think the coolest thing a mathematician can do is to create a more interpretable lean.
Lots of complaints about how lean proofs are unreadable - then create your own high level lang that compiles down into lean or have your own verifier.
If this works, then all future AI proofs have a strong incentive to go through your thing.
Might be one of the few big math infra projects, though arguably humans may want to curate the proof/lemma ontologies for interpretability.
i think my steelman for yud is that AI takeover only needs to work once for humanity to be screwed, much like how cancer only needs to win once to kill you.
More options
Context Copy link