Justin Sun Prize Spotlight Details How Neel Somani Solved Two Problems

The Justin Sun Prize’s Oct. 28 Winner Spotlight detailed how prize winner Neel Somani used GPT 5.2 Pro on one problem and organized undergraduates to tackle another.

The prize confirmed Somani’s solutions to JSP-000327 and JSP-000239 on Oct. 14. The spotlight added details about how he approached the two problems, from checking a model-assisted effort to coordinating a student search across open questions.

JSP-000327 asks whether only finitely many equalities exist between products of distinct central binomial coefficients under specified restrictions. Somani entered the problem into GPT 5.2 Pro, then checked the algebra by hand. Mathematician Daniel Larsen verified the submission, and Harmonic’s Aristotle tool produced a formalization in Lean, a proof assistant.

JSP-000239 asks whether an infinite cover made up of residue classes can be approximated uniformly in density by a finite subcollection. Somani formed a team of undergraduates from UC Berkeley, Northwestern and Rice. The group used large language models to search open problems on the Erdős problem list and turned to Aristotle for Lean formalization when needed. Somani documented the work and organized failed attempts to show where the models struggled.

Somani’s work focuses on machine learning and formal verification. He completed majors in mathematics, computer science and business at UC Berkeley, worked as a quantitative researcher at Citadel, and has published papers in USENIX Security and OOPSLA. He also used Lean to identify a performance regression in CPython’s sorting algorithm. Somani has described formalization as a way to constrain software correctness as well as verify mathematics.

The prize credits Somani as the Mathematical Solver for both problems and tracks Lean Formalizer as a separate role. Each problem’s award is divided between those roles: 70% for the solver and 30% for the formalizer. A person who performs both roles can receive the full award.