3 ms·
I'm not sure the lean coverage of pure math research is that much (maybe like 1% is represented on mathlib). But I think a system like alpha proof could even to
by Davidzheng 2y ago
I'm not sure the lean coverage of pure math research is that much (maybe like 1% is represented on mathlib). But I think a system like alpha proof could even today be useful for mathematicians--I mostly dislike systems like o1 where they confidently say nonsense with such high frequency. But i think value is already there.
- lanstin 2y agoThe point about using lean is you don't have to trust you can verify.
- Davidzheng 2y agono I agree I just don't think existing Lean codebase is approaching useful coverage. Should change soon
- lanstin 2y agoI keep asking people in my department about using lean but zero interest so far.