Comment on Why mathematics is set to be revolutionized by AI
Audalin@lemmy.world 8 months ago
The article isn’t about automatic proofs, but it’d be interesting to see a LLM that can write formal proofs in Coq/Lean/whatever and call external computer algebra systems like SageMath or Mathematica.
CapeWearingAeroplane@sopuli.xyz 8 months ago
I was thinking something similar: If you have the computer write in a formal language, designed in such a way that it is impossible to make an incorrect statement, I guess it could be possible to get somewhere with this