ByteDance Launches Seed Prover 1.5: New Advancements in Formal Mathematical Reasoning

Recently, the Seed team at ByteDance launched its latest formal mathematical reasoning model, Seed Prover 1.5, marking a significant breakthrough in the field of mathematical reasoning. This release was made possible by in-depth exploration of large-scale Agentic reinforcement learning, significantly improving its reasoning capabilities and efficiency.

During the 2025 International Mathematical Olympiad (IMO), Seed Prover demonstrated its powerful performance. Within just three days, the model successfully solved four out of six problems and provided partial proofs for one, ultimately earning an official silver medal. In comparison, Seed Prover 1.5 generated complete, compilable, and verifiable Lean proof code for the first five problems of IMO2025 within 16.5 hours, meeting the standard for a gold medal.

More notably, Seed Prover 1.5 also performed outstandingly in the 2025 Putnam Mathematical Competition, completing 11 out of 12 problems by generating compilable and verifiable Lean code within 9 hours. This achievement set new records for formal mathematical reasoning models across multiple evaluation sets, especially in assessments with math difficulty levels comparable to those of master's and doctoral students, where it solved 80% and 33% of the problems respectively.

The innovation of Seed Prover 1.5 lies in its new Agentic Prover architecture, which combines the advantages of natural language reasoning and formal proofs. Unlike previous formal provers, Seed Prover 1.5 can flexibly call various tools during the proof process, such as actively retrieving the extensive mathematics library Mathlib and executing Python code to assist verification. Through incremental lemma verification, the model breaks down complex problems into several lemmas and gradually builds formal proofs.

Additionally, Seed Prover 1.5 introduced the Sketch Model, which simulates the problem-solving approach of human mathematicians, transforming natural language proofs into high-level proof frameworks, thus significantly reducing the difficulty of proving complex theorems. By adopting this "divide and conquer" strategy, Seed Prover 1.5 can effectively avoid error accumulation when generating long texts.

Technical Report:

https://arxiv.org/abs/2512.17260

Lean Proof Code:

https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip

ZTE Invests in AI Phones! Collaborates with ByteDance to Launch Doubao Phone, Open Ecosystem May Enter an Era of Multiple Models Coexistence

ZTE and ByteDance have collaborated to launch the Doubao phone, aiming at the future of AI phones. Both parties, based on the concept of "openness as innovation," are jointly building their presence in the AI field. ZTE said this is just the beginning, and it has already received cooperation invitations from multiple large model manufacturers, and is currently building a diverse AI ecosystem.

Jan Team Releases Jan-v2-VL-Max! A 30B Multimodal Model Specializing in Long-Term Agent Tasks, Stable Execution of Long Sequences Outperforms Gemini 2.5 Pro

The Jan Team releases the 30B-parameter multimodal large model Jan-v2-VL-Max, designed for long-term and highly stable automation tasks. Its performance surpasses Google's Gemini 2.5 Pro and DeepSeek R1. The model focuses on solving the 'error accumulation' and 'loss of focus' issues in multi-step tasks, providing strong support for the open-source agent ecosystem.

Alibaba Launches Qwen ZhiXue, ByteDance Introduces AnyGen: AI Applications Take Over Your Backpack and Desk

Alibaba has launched the AI education application "Qwen ZhiXue," while ByteDance has introduced the AI productivity tool "AnyGen" overseas, indicating that major tech companies are accelerating the application of AI technology in vertical scenarios. The competition between the two giants in the fields of AI personalized services and lightweight productivity has fully escalated.

From Red Envelope Battles to AI Competitions: Huoshan Engine May Become the Exclusive Partner of the 2025 CCTV Spring Festival Gala

Huoshan Engine, a subsidiary of ByteDance, has become the exclusive AI cloud partner of the 2026 CCTV Spring Festival Gala. Its intelligent assistant, "Doubao," will be deeply involved in the interaction. As a national-level IP, the Spring Festival Gala is a key battlefield for internet products to achieve explosive growth. ByteDance's move aims to replicate the successful model of WeChat Pay and other companies that broke through via the Spring Festival Gala.

GPT-5 First Successfully Solves a Mathematical Problem Independently, Transparent Attribution Experiment Sparks Academic Debate

Swiss mathematician Schmidt announced that GPT-5 has, for the first time without human intervention, independently solved a long-standing unsolved mathematical problem. Its solution demonstrated remarkable creativity, borrowing techniques from other branches of algebraic geometry rather than following conventional logic. This breakthrough confirms Terence Tao's prediction about the potential of AI.