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
You are not logged in. However you can subscribe from another Fediverse account, for example Lemmy or Mastodon. To do this, paste the following into the search field of your instance: !technology@lemmy.world
This is a most excellent place for technology news and articles.
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