Zheng Yuan

Excited to announce Seed-Prover 1.5 which is trained via large-scale agentic RL with Lean. It proved 580/660 Putnam problems and proved 11/12 in Putnam 2025 within 9 hours. Check details at github.com/ByteDance-Seed…. We will work on autoformalize towards contributing to real math!

Congrats!

@ElliotGlazer Irrationality of zeta(3) github.com/ahhwuhu/zeta_3…

FLT PNT with effective bounds The weak Goldbach conjecture Infinitude of prime pairs of gap \le 246 Baker's theorem restricted to computable reals Irrationality of zeta(3) CFSG The quasi-polynomial time algorithm for Graph Isomorphism PL Poincaré Conjecture in dimensions =/= 4.

Prediction: each of the following theorems will have *axiom-free* proofs in Lean within the next 5 years: 🧵

@ahmedsameh0__0 dm me your cv

Finally got 10k citations.

I proof riemann hypothesis using native_decide 🤡: import Mathlib def foo : Bool := withPtrEq True False (fun () => false) fun eq => nomatch cast eq ⟨⟩ theorem f : False := nomatch show foo = true by native_decide theorem anything : RiemannHypothesis := by exfalso exact f

This is the arxiv: arxiv.org/abs/2512.17260

Excited to announce Seed-Prover 1.5 which is trained via large-scale agentic RL with Lean. It proved 580/660 Putnam problems and proved 11/12 in Putnam 2025 within 9 hours. Check details at github.com/ByteDance-Seed…. We will work on autoformalize towards contributing to real math!

@linexjlin 你好 我认为lean模型和自然语言的有效上下文长度不具备直接可比性

字节的论文提到一个问题：上下文不够用了 Seed-prover 1.5 的论文里提到他们的 Lean 证明器生成的 32K-64K 长度的证明中错误占了多数，获得了持续性负分（答对1 分，答错-1分），表现出在超长 CoT 情况下解题能力退化 （见图4d）。 相比起来 DeepSeek-Speciale 的就应对自如。复杂编程任务平均每题 77k 几乎占快占满了 128K 上下文了。 这可能是注意力机制的问题。 Seed-prover 训练自 seed-1.6 用的应该是 GQA， Deepseek 用的是 DSA。

@chijinML Thank you ❤️

This is a truly remarkable math theorem prover! — well ahead of competitors, near-saturating PutnamBench, and achieving much higher solve rates on the recent concluded Putnam 2025 with a suprisingly short amount of time.

@WendaLi8 Thank u!

Congratulations to the Seed team. The field is progressing so fast!

@AlbertQJiang @huajian_xin @regunivers @hanwen_zhu Thank u! Looking forward to yours!

@GanjinZero @huajian_xin @regunivers @hanwen_zhu Incredible work, congrats!!!

@JasonRute @ElliotGlazer using reasoning model to get correct answer is quiet easy for Putnam

@ElliotGlazer But for the most recent Putnam, I would hope that (just like the previous IMOs) the teams would also automatically find the answer. In my humble opinion, none of Axiom, Harmonic, or Seed Prover have been very forthcoming with how they do this for Putnam 2025.

Been waiting for this one. Looks like we’re eating good this weekend boys 😋

@shi_wenlei 🎉

Today we released Seed-Prover 1.5, which masters the undergraduate-Level math theorem proving by agentic LLM and test-time scaling🥳🥳🥳 github.com/ByteDance-Seed…

@AIYangMing @huajian_xin @regunivers @hanwen_zhu Thank u!

@GanjinZero @huajian_xin @regunivers @hanwen_zhu Congratulations!

@Teknium @huajian_xin @regunivers @hanwen_zhu Same as seed-1.6

@GanjinZero @huajian_xin @regunivers @hanwen_zhu How big is the model?

@lalalaepsilon @huajian_xin @regunivers @hanwen_zhu We don’t test on non formal yet

@GanjinZero @huajian_xin @regunivers @hanwen_zhu Does it generalize to non formal reasoning as well ?

@allanjienlp scaling!

keep scaling!📈

@nopainkiller merry christmas

Christmas!

@nasqret I found sorry in this formalization. I think IsIntPoly_div_by_monic has not been finished and lots of theroems are relied on it. We cannot call this paper been formal verified.

Mathematical papers need formal validation. This is usually done informally by a referee. But what if we could rely on something more robust like auto-formalization into Lean 4 where the role of the referee would be reduced to meticulous checking of the formulations of the definitions and theorems? The compilation of automatically generated code would become a proof certificate. This is what happened in a longer run which I did with Aristotle by @HarmonicMath. Thanks to @PietroMonticone and @llllvvuu for helping with the setup for the blueprint. Here I present a complete correct auto-formalization of a paper of my friend Stefan Barańczuk about Chebyshev divisiblity sequences. The code is about 5000 lines of highly non-trivial Lean. It corrects all the inconsistencies and gaps in the main paper (even proving some delegated propositions). nasqret.github.io/ZsigmondyCheby… I am gonna post a series of such experiments, proving that in some areas of mathematics, including elementary number theory, combinatorics and analysis (all sorts of things covered by Mathlib) we are not far from a massive shift in documentation of validity of proofs. I think this is going be a hectic year!

Will be at NIPS from Dec 2~6, find me to talk about formal math reasoning & seed prover.