# 08/01/25: Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification with Kaiyu Yang

Page: https://stenobird.com/podcast/boston-computation-club-4031660/08-01-25-formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification-with-kaiyu-yang
Text version: https://stenobird.com/podcast/boston-computation-club-4031660/08-01-25-formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification-with-kaiyu-yang.md
Podcast: [Boston Computation Club](https://stenobird.com/podcast/boston-computation-club-4031660)
Published: 2025-08-02T20:11:16+00:00
Episode link: https://podcasters.spotify.com/pod/show/bostoncc/episodes/080125-Formal-Reasoning-Meets-LLMs-Toward-AI-for-Mathematics-and-Verification-with-Kaiyu-Yang-e36c7au
Audio file: https://anchor.fm/s/5eee01ac/podcast/play/106355486/https%3A%2F%2Fd3ctxlq1ktw2nl.cloudfront.net%2Fstaging%2F2025-7-2%2F5eacdd3f-2530-1303-94cb-5fa9f65921f2.m4a
Processing state: not_requested
JSON: https://stenobird.com/v1/public/podcasts/boston-computation-club-4031660/episodes/08-01-25-formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification-with-kaiyu-yang
Duration seconds: 4414

## Resource

Today Kaiyu Yang from Meta joined us to discuss formal reasoning using LLMs, particularly in the context of interactive theorem provers. This is a really fast-moving and exciting field in which reinforcement learning and theorem proving combine to provide a new frontier for fully automated reasoning, and Kaiyu is at the bleeding edge of it. We were really lucky to get an hour of Kaiyu's time and we hope you enjoy the talk as much as we did!

## Actions

- request_transcript: `POST https://stenobird.com/v1/public/podcasts/boston-computation-club-4031660/episodes/08-01-25-formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification-with-kaiyu-yang/transcription-requests` — Idempotently request low-priority transcript generation for this episode.
- read_markdown: `GET https://stenobird.com/podcast/boston-computation-club-4031660/08-01-25-formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification-with-kaiyu-yang.md` — Read the agent-friendly Markdown representation of this episode resource.

A page view does not enqueue transcription. Agents should invoke `request_transcript` explicitly when they need this episode processed.

## Transcript

Full transcripts are not published on public pages unless there is a clear rights basis.