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.
you are viewing a single comment's thread
view the rest of the comments
view the rest of the comments
replies: