Harmonic (@HarmonicMath)

Aristotle Agent라는 '자율 수학자' 모델이 공개되어 현재 라이브로 무료 제공 중이라고 발표되었다. 해당 에이전트는 복잡한 수학 연구 문제를 해결·형식화하도록 설계되었고, 게시물에 따르면 'Formal Math' 분야에서 1위 성과를 기록했다는 주장도 포함되어 있다. 수학 연구용 에이전트형 AI의 새로운 응용 사례로 주목됨.

https://x.com/HarmonicMath/status/2034028065513451594

#aristotleagent #autonomousagent #formalmath #mathai

We’re pleased to announce #ItaLean2025: Bridging Formal Mathematics and AI, an international conference dedicated to @leanprover, Formal Mathematics, and AI4Math.

📍 University of Bologna
🗓 9–12 December 2025

#ItaLean2025 brings together researchers and practitioners advancing the formalization of mathematics in Lean and exploring the interplay between machine learning and formal methods.

The program includes lectures, tutorials, research talks, product demos, and a concluding panel.

Applications to participate are now open.
Participation is free of charge.

A limited amount of travel support may be available.
Priority deadline: 31 October 2025.

A preliminary schedule will be released in the coming weeks, with regular updates to follow.

Official website (applications, program, logistics): https://pitmonticone.github.io/ItaLean2025/

#LeanLang #FormalMath #AI4Math