Auto-Solving Mathematical Proofs

Stream: general

[Sovan Sahoo]

can use lean to automatically find solutions to very basic mathematical questions like probability ?

[Jireh Loreaux]

Probably not. Lean is not an automated theorem prover, it is an interactive theorem prover. But it depends precisely on what you mean by very basic.

[Sovan Sahoo]

"A sum of money amounts to $8,820 in 2 years at simple interest. If the principal had been $500 more, the amount would have been $9,450 in the same period. What is the rate of interest per annum?"

if questions like these are formalized into leancode ,what assitance can lean provide me to solve it?

[Kevin Buzzard]

Are you able to turn this into Lean code yourself? But my impression is that you have very much the wrong idea about what Lean is. This looks like the kind of question a language model might be quite good at.

[Sovan Sahoo]

Ya,i can understand that llms can be used ,but for slightly complex mathematical questions where llms fail ,can lean chip in to provide some assistance to solve the question or is it simply a validation platform for proofs?

[Kevin Buzzard]

It's simply a validation platform for proofs.

[Kevin Buzzard]

There is work on getting LLMs to write Lean code (e.g. by DeepMind), but that's not Lean's problem, that's the LLM's problem.

[Sovan Sahoo]

ya i have read about few data sets with parallel pairs of informal and formal component that can be used to fine tune llms.
But if lean is an interactive platform ,does it auto suggest the tactics that should be used to solve a theorem?

[Kevin Buzzard]

No.