| CARVIEW |
Select Language
HTTP/2 301
server: GitHub.com
content-type: text/html
location: https://mathai2025.github.io/schedule/
access-control-allow-origin: *
strict-transport-security: max-age=31556952
expires: Mon, 29 Dec 2025 13:52:59 GMT
cache-control: max-age=600
x-proxy-cache: MISS
x-github-request-id: 66D4:15317B:8E6B67:9FCE67:69528562
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 13:42:59 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210036-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767015780.599727,VS0,VE207
vary: Accept-Encoding
x-fastly-request-id: b2e86ed1af1089b7ca292037cd78a4eab0306663
content-length: 162
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Sat, 06 Dec 2025 06:01:35 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"6933c6bf-2a69"
expires: Mon, 29 Dec 2025 13:52:59 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: BB1B:2680BD:8DD0A0:9F328F:69528563
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 13:43:00 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210036-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767015780.835785,VS0,VE221
vary: Accept-Encoding
x-fastly-request-id: 0e3e1a0e976a6634b682082c3d75512053be05d3
content-length: 3678
5th MATH-AI Workshop at NeurIPS'25 - Math-AI
The 5th Workshop on Mathematical Reasoning and AI
MATH-AI
The 5th Workshop on Mathematical Reasoning and AI
Schedule
All times are in Pacific Time (PT)
| 8:25am - 8:30am | Opening Remarks |
| 8:30am - 9:00am | Invited Talk: Weiyang Liu (Chinese University of Hong Kong), "Scalable Formal Verification Enables Novel Design" |
| 9:00am - 9:30am | Invited Talk: Hannaneh Hajishirzi (UW & AI2), "Olmo 3 Model Flow for Mathematical Reasoning" |
| 9:30am - 10:00am | Invited Talk: Max Tegmark (MIT), "Vericoding: Formally Verified Program Synthesis" |
| 10:00am - 10:30am | Invited Talk: Leonardo de Moura (Lean FRO & AWS), "Teaching AI to Configure Proof Automation in Lean" |
| 10:30am - 11:15am | Panel Discussion: Tengyu Ma (Stanford), Tom Kalil (Renaissance Philanthropy), Patrick Shafto (DARPA & Rutgers), Jonathan Thomm (Harmonic) |
| 11:15am - 12:00pm | Poster Session 1 |
| 12:00pm - 1:00pm | Lunch Break |
| 1:00pm - 1:30pm | Invited Talk: Aviral Kumar (CMU), "The Various Dimensions of Scaling RL for Improving Math Reasoning" |
| 1:30pm - 2:00pm | Invited Talk: Weizhu Chen (Microsoft), "From One Shot to Self-Play: Evolving RL-Based Reasoning Data in LLMs" |
| 2:00pm - 2:30pm | Coffee Break |
| 2:30pm - 3:30pm | Contributed Talks ∙ Sumanth Varambally: "Hilbert: Recursively Building Formal Proofs with Informal Reasoning" ∙ Sergey Galkin and Igor Kiselev: "CayleyPy Growth: Efficient growth computations and hundreds of new conjectures on Cayley graphs" ∙ Yuxiao Qu: "Learning to Reason on Hard Problems with Privileged On-Policy Exploration" |
| 3:30pm - 4:15pm | Panel Discussion: Swarat Chaudhuri (UT Austin & Google DeepMind), Jasper Dekoninck (ETH Zürich), Chi Jin (Princeton), Dawn Song (UC Berkeley) |
| 4:15pm - 5:25pm | Poster Session 2 |
| 5:25pm - 5:30pm | Closing Remarks |