Warning: Some posts on this platform may contain adult material intended for mature audiences only. Viewer discretion is advised. By clicking ‘Continue’, you confirm that you are 18 years or older and consent to viewing explicit content.
Cheap data and the absence of coincidences make maths an ideal testing ground for AI-assisted discovery — but only humans will be able to tell good conjectures from bad ones.
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.
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
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.
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