Experiences of Generating Formal Proofs with LLMs

▶︎ Topic: Experiences of Generating Formal Proofs with LLMsIn recent years, AI/LLM has developed rapidly, capable of generating not only text and images but also stable code. A few months ago, cutting-edge models like GPT 5.4 and Claude Opus 4.6 began to generate relatively complex formal mathematical proofs, even for complex correctness of compiler intermediate representation transformations, simply by providing a similar proof "template" to produce correspondingly phrased formal proofs.This talk will explore the experience of using the GPT 5 series and Agda to write dependently typed programs and formal theorem proofs, demonstrating how language models, through the assurances of theorem provers, generate mathematically sound proofs of correctness that are nearly flawless.▶︎ Presenter: Chen Liang-Ting, an assistant researcher at the Academia Sinica, enjoys trying various new things. His recent interests include type theory, categorical models, and proofs with computational significance.*This time the event starts earlier! It begins at seven o'clock!----------------The event is free, and donations to the venue g0v are welcome. Just walk right in.You are welcome to come for交流、交朋友！