孫宇晨獎官方以 Winner Spotlight 確認 Neel Somani 為最新獲獎人，成功解出 JSP-000239、JSP-000327 兩道數學題，並公開其以大型語言模型與 Lean 形式化協作的解題路徑。
（前情提要：孫宇晨獎公示期圓滿結束，首批獲獎人確認、獎金發放正式啟動）
（背景補充：孫宇晨宣布設立「孫宇晨獎」 開啟機器驗證數學懸賞新紀元 最高獎金100萬美元）
繼動區 10 月 5 日報導指出題庫第 239、327 號解題候選於 9 月 30 日進公示、當時仍進行中之後，孫宇晨獎官方帳號 @JustinSunPrize 於台北時間 10 月 28 日晚間刊出 Winner Spotlight，確認 Neel Somani 為最新獲獎人，並把兩題怎麼解、誰驗證、何時從候選移入獲獎名冊一次講清楚。
官網 laureates 已將他列為 JSP-000239、JSP-000327 的 Mathematical Solver（2026），角色是解題者，與 Lean Formalizer 分開登錄。早在 10 月 14 日，官方就已發文祝賀兩題過關；孫宇晨本人同日於 X 轉發，指兩題已解出並經形式化驗證。本篇 Spotlight 補上解題現場與人機協作細節：模型怎麼用、誰當夜驗證、本科生團隊怎麼掃開放題，焦點放在現場，而不是重講 9 月設獎故事。
兩題怎麼解：從貼進 GPT，到組本科生掃題
依官方 X Article，Somani 專攻機器學習與形式化驗證，UC Berkeley 數學、資工、商管三主修，曾任 Citadel 量化研究員，論文見於 USENIX Security、OOPSLA。他近期還用 Lean（形式化證明助手）揪出 CPython 排序演算法效能倒退。
第一題 JSP-000327：在所述限制下，相異中央二項式係數乘積之間的等式是否僅有有限多個？這是他解出的第一道 Erdős（艾狄胥）題。Spotlight 寫他把題目貼進 GPT 5.2 Pro（大型語言模型），因屬組合學陳述，再手動核對代數是否站得住；投稿論壇後，當晚由數學家 Daniel Larsen 驗證，隨後 Harmonic 產品 Aristotle 產出 Lean 形式化。
第二題 JSP-000239：無限剩餘類覆蓋能否用有限子族在密度上均勻逼近？初戰得手後，他組起含 UC Berkeley、Northwestern、Rice 等校本科生的團隊，系統用 LLM 掃過 Erdős 網站上的開放題，必要時再以 Aristotle 形式化；結果寫在其部落格，並整理一套失敗案例本體論，方便後人看見模型卡在哪。他感謝孫宇晨團隊支持，並形容過去一年 AI 數學進展「incredible」，也提到形式化不只驗數學、還能約束軟體正確性。
從候選到上榜：14 天公示與獎金邊界
GitHub awards 倉庫 #5051 顯示，兩題解題候選於 9 月 30 日登記後進入公示，10 月 14 日正式移入獲獎名冊；同日 官方與 @justinsuntron 先後公開祝賀。合併進名冊、公示期屆滿本身仍不等於立刻撥款，獲獎人還須完成書面確認與請款流程；身份與收款資訊走官方信箱，不在 GitHub issue 公開貼錢包地址或私鑰。
依官方 FAQ，單題獎金拆解題 70%、Lean 形式化 30%；若同一人同時扛兩個角色可拿全額。頂層 Pinnacle 為 100 萬美元，其餘層級金額以各次公告為準，並以 USDT（TRC20）或 USDC（ERC20）發放，候選通常經 14 天公示。本次 Spotlight 聚焦解題路徑與人機協作，也未寫出他兩題對應的具體美元數額。
想跟題、看規則或提交解法，可上 孫宇晨獎官網 About；題庫與獲獎紀錄也在 GitHub 組織 TheJustinSunPrize 公開。口號仍是：Quod probatur, solvitur —— 能被證明者，即被解決。
📍相關報導📍
孫宇晨宣布設立「孫宇晨獎」 開啟機器驗證數學懸賞新紀元 最高獎金100萬美元
