video

1 view

Skip to first unread message

Alexander Shen

unread,

Sep 29, 2025, 6:13:31 PMSep 29

to Kolmogorov seminar on complexity, Akim Kumok, Alla & Alexandre Zvonkine

https://youtu.be/pRQGgmRseMk (00:11:30 - 02:11:00 approximately)

Announcement from the speaker: In the past few years, LLMs went from generating text that only look reasonable to generating correct solutions to IMO problems and, in some cases, research problems. On the other hand, in many cases LLMs still prefer to hallucinate rather than admit failure. How one can trust LLM-produced proofs? One of the answers to this question is to make an LLM produce a proof that can be formally verified by a computer. In my talk, I will discuss the following questions: - What is Lean? How do definitions, theorem statements, and proofs look like? - How does it help LLMs solve math problems? - What other tools can an LLM use? - Can an LLM learn a new skill based on a limited amount of information?

Reply all

Reply to author

Forward

0 new messages