Talk by Hsin-Yuan Huang (Oratomic, Caltech)
summary
Argues that large language models plus persistent memory and multi-agent verifier loops already solve many self-contained theory problems: cites the MemGPT literature on MemGPT persistent memory, examples of frontier models one-shotting QIP-style papers, Robin Kothari’s bag of open problems being solved, agents from Victor Albert proving long-standing theorems, and a concrete scenario where a 20-agent pipeline with $2,000 produces idea X and surprising result Z mid-talk. Proposes formal verification and Lean-verified proofs plus ownership, choice and dream as policy levers.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:14Sacredness of research and AI concerns
- 4:05AI existential crisis
- 7:23Against full automation
- 13:55Automating research with AI
- 23:25Credit in AI discoveries
- 36:28Research beyond results
- 59:05Human value in research
- 1:04:06Open research questions
- 1:14:02Q&A
related talks
43mPanel Discussion
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
15mToward A Quantum Programming Language for Higher Level Formal Verification
21mAnalyzing quantum programs using the power of interaction
21mInteractive Proofs for Synthesizing Quantum States and Unitaries
27mParameterized Verification of Quantum Circuits
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
01h 31mLightning Talks