The Seed team at ByteDance has recently made an exciting announcement regarding the launch of Seed Prover 1.5, a model specifically tailored for formal mathematical reasoning. According to the provided introduction, when compared to its previous version, Seed Prover 1.5 has demonstrated remarkable capabilities. It successfully generated complete and compilable Lean proof codes for the first five problems of the International Mathematical Olympiad (IMO) 2025 within a mere 16.5 hours. When these results were converted into a scoring system, it achieved an impressive score of 35 out of 42, a mark that already surpasses the threshold required to secure a gold medal at the IMO. Presently, the technical report detailing the features and advancements of Seed Prover 1.5 has been made available to the public. Moreover, plans are underway to open up an API in the near future, providing mathematicians and AI researchers with an opportunity to directly experience and explore the capabilities of this innovative model.