在洪樂潼心中，「AI數學家」的終極意義藏在一個古老的故事裏。「你看過傳記電影The Man Who Knew Infinity（港譯《數造傳奇》）嗎？」洪樂潼接受媒體採訪時表示，電影主角拉馬努金是一位印度天才。他從未接受過正規的證明訓練，僅憑直覺便在草稿紙上寫滿了令人驚嘆的數學猜想。遇到數學家哈代和利特爾伍德後，拉馬努金才開始學習怎麼證明。

「我們的夢想是數學發現本身」

「如果世界上某個角落有一個拉馬努金，那麼『AI數學家』能夠幫助他完成證明，讓他有更多時間和能量去完成下一個直覺的發現。」洪樂潼說，「我們的夢想，其實是數學發現本身。」

洪樂潼的夢想，與AI科技前沿密不可分。在求學期間，洪樂潼就嗅到了創業的機會。2024年秋天，一種名為Lean的語言進入她的視野。與自然語言不同，Lean語言是一個非常神奇的、可以自驗證的數學編程語言。洪樂潼打了個比方：「如果用英語寫出數學證明，我沒辦法知道一個5000行的證明是否正確，需要找高水平的專家驗證。但Lean是自驗證的，只要跑通了就是對的。」

2025年1月，在美國最大的數學家聚會──2025年聯合數學會議（JMM）上，洪樂潼見到了許多做Lean語言的數學家。她意識到，「AI數學家」有可能從科幻變成現實。當年10月，在Axiom Math完成6400萬美元（約5億港元）融資後，洪樂潼放棄了博士學位，全身心投入了創業。她的團隊，也成了一匹飛速奔跑的「黑馬」。

2025年12月3日，洪樂潼在社交平台發文，宣布其公司開發的AxiomProver系統，分別用1天和5小時，在無人為干預的情況下解決了兩道數學難題──埃爾德什問題集中第124題和第481題的證明。「我真正感受到了一個AI時刻，有些事情和昨天不一樣了。正如AI解決蛋白質折疊問題一樣，『AI數學家』是送給人類的禮物！」\大公報記者盧靜怡