{"podcast":{"title":"Boston Computation Club","slug":"boston-computation-club-4031660","podcast_index_feed_id":4031660,"rss_url":"https://anchor.fm/s/5eee01ac/podcast/rss","website_url":"https://podcasters.spotify.com/pod/show/bostoncc","image_url":"https://d3t3ozftmdmh3i.cloudfront.net/production/podcast_uploaded_nologo/15826563/15826563-1623263635731-99a8ec66007e4.jpg","author":"Max von Hippel","episode_count":89,"summary":"The Boston Computation Club is a small seminar group focused on mathematical computer science, and computational mathematics. Its name is plagiarized from the London Computation Club. Boston Computation Club meetings occur roughly every other week, on weekends, around 5pm EDT (modulo speaker availability). The usual format is a 20m presentation followed by 40m of discussion. Some, but not all, meetings are posted on YouTube and in podcast form.","last_synced_at":"2026-09-08T12:21:35.234206+00:00","page_url":"https://stenobird.com/podcast/boston-computation-club-4031660"},"episode":{"title":"08/01/25: Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification with Kaiyu Yang","slug":"08-01-25-formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification-with-kaiyu-yang","published_at":"2025-08-02T20:11:16+00:00","page_url":"https://stenobird.com/podcast/boston-computation-club-4031660/08-01-25-formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification-with-kaiyu-yang","show_page_url":"https://stenobird.com/podcast/boston-computation-club-4031660","url":"https://podcasters.spotify.com/pod/show/bostoncc/episodes/080125-Formal-Reasoning-Meets-LLMs-Toward-AI-for-Mathematics-and-Verification-with-Kaiyu-Yang-e36c7au","audio_url":"https://anchor.fm/s/5eee01ac/podcast/play/106355486/https%3A%2F%2Fd3ctxlq1ktw2nl.cloudfront.net%2Fstaging%2F2025-7-2%2F5eacdd3f-2530-1303-94cb-5fa9f65921f2.m4a","summary":"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!","meta_description":"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…","key_points":[],"chapters":[],"topics":[],"duration_seconds":4414,"processing_state":"not_requested","actions":[{"name":"request_transcript","method":"POST","url":"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","description":"Idempotently request low-priority transcript generation for this episode."},{"name":"read_markdown","method":"GET","url":"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","description":"Read the agent-friendly Markdown representation of this episode resource."}]}}