DAC Economy

seeing this progress from @AnthropicAI makes me reflect on Valida - the zk prover my team built. it’s encouraging to see zk finding its place. i hope we still contributed something valuable along the way and helped move the field forward!

openai released 722 math manuscripts today. 372 result families, ~4,000 problems posed, about three hours of compute each, from one internal model. not all are formalized yet; the readme says some unformalized results "could have issues." nobody has read most of them. this is the proof abundance terence tao warned about at icm, and it arrived in a single commit. github.com/openai/math tao's point: a result goes through generation, verification, exposition, publication, canonicalization before it counts as mathematics. ai is good at the first and getting good at the second. the other three are slow and human. the bottleneck isn't finding proofs anymore, it's digesting them. a lean-checked proof nobody understands is correct but useless, and openai's repo has 722 of them, some not even lean-checked. i think this post could be a solution. it attempts to turn "mathematical understanding" into something you can train on, and it points at a better reward than anything provers use today. oleg's idea here is to freeze a smaller model, fix its compute, hand it a theory, count what it can derive now that it couldn't before. it's a measurable version of understanding, and it's basically tao's digestion stage as a number. and that number is a reward. every prover we train today gets paid for "proof accepted." self-play setups pay the conjecturer by the prover's pass rate. both optimize for volume of provable statements, which is the stage we already have too much of. if the reward is halo delta instead, a proof is worth nothing on its own. it only gets credit when it finds structure that makes unseen theorems cheaper. that's compression, and nobody has shown how to train it at scale yet. the closest attempt is from @AIatMeta two weeks ago (patel, rammal, hayat, munos, kempe, "learning to discover interesting mathematics" @niketnpatel @KempeLab). they define a theorem's interestingness as proof length over statement length, train a 27b model to predict proof difficulty given premises, and grpo a conjecturer against that score. mathlib overlap drops from 92% to 31%. they also define a utility measure, lines of lean saved across the library when the theorem is added, and show it correlates with interestingness. that utility is a halo. but it's static, computed over an existing library, and they train on interestingness rather than on utility directly. oleg's version makes the halo relative to a bounded reasoner on unseen theorems and trains on it. that's the difference. rough shape would be: an explorer generates proofs at volume. a compressor turns piles of them into definitions and key lemmas, trained on halo delta. a frozen student is the instrument. the compressor is the model whose reasoning you actually care about. library-learning systems have mostly accumulated lemmas with little reuse under matched compute. my guess is that's because nobody has trained the compressor with a transfer reward. there was no signal to train on. this gives you one open questions: how big the student should be. whether halo delta on lean theorems tracks what mathematicians call insight etc. and the obvious ablation now that a baseline exists: does model-relative halo beat fair's static utility as a training signal