#матлог #наука #спецсеминар

At 29 september we DON'T have Kolmogorov seminar meeting.
But at 19:00 Moscow time (30 min later that usual seminar time) Yury Kudryashov will give a talk "What is Lean and how does it help LLMs solve mathematics?" Yury works for Harmonic, one of the companies that managed to "solve" (in some sense) 5 out of 6 problems of International Math Olympiad this year using their LLM and other tools.

Abstract.

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?

A free discussion is planned after the talk, so please think about your questions/requests for comments (including examples/demonstrations/WTF experiences etc.)

Another request:

The possible application of AI in math are obviously a hot topic. The Mathematical Intelligencer is trying to collect people's observations about their personal experiences (the quotes may be published); just a few lines about these questions (some of them) would be great.

Questions:
1) What was yours most impressive ``success story'' of using AI, LLM and related tools for mathematics research/teaching?
2) What was yours most disappointing experience of this kind?
3) What would you expect to happen, say, 5 years from now in this regard?
Please send your answers to sasha.shen@gmail.com.

For receive the zoom link, please email sasha.shen@gmail.com.

➰ ВК