Prove2Me가 여는 Lean 4 형식화 협업, 사람과 AI 에이전트는 어떻게 함께 일하나 | DAKER 커뮤니티
형식 검증된 수학은 오래전부터 가능성을 보여 왔지만, 실제로 규모 있게 쌓아 올리는 일은 늘 높은 장벽 앞에 멈추곤 했습니다. Lean 4 같은 증명 보조기를 다루는 기술, 수학적 배경지식, 그리고 긴 작성 시간이 함께 필요했기 때문입니다.
2026년 8월 28일 arXiv에 공개된 Prove2Me는 이 장벽을 사람과 AI 에이전트의 협업으로 낮추려는 시도입니다. 오늘 글은 arXiv:2608.28433의 초록이 말하는 범위 안에서, 이 플랫폼이 무엇을 제안하는지 정리합니다.
논문 제목은 Prove2Me이며, 저자는 Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng입니다. 플랫폼 주소는 https://prove2.me이고, PDF는 https://arxiv.org/pdf/2608.28433에서 볼 수 있습니다. 이 글은 초록에 적힌 내용만 다루며, 초록에 없는 사용자 수나 증명 개수 같은 통계는 포함하지 않습니다.
형식화의 진입 장벽을 낮추는 방식
Lean 4 같은 증명 보조기는 수학적 내용을 기계가 검사할 수 있는 형식으로 옮기게 해 줍니다. 다만 대규모 형식화는 형식 검증에 대한 이해와 수학 전문성, 그리고 긴 작성 시간을 함께 요구해 왔습니다.
Prove2Me가 주목하는 변화는 AI 코딩 에이전트입니다. 초록에 따르면, 이 에이전트들은 자연어 프롬프트를 바탕으로 복잡한 Lean 증명을 작성할 수 있고, 그 결과 형식화의 진입 장벽이 크게 낮아졌습니다.
사람과 AI 에이전트가 함께하고, 올바름은 기계가 검사하는 인터넷 규모 협업의 가능성이 열리고 있습니다.
이 지점에서 Prove2Me는 단순한 자동화 도구라기보다, 수학 형식화를 위한 개방 협업 플랫폼으로 제시됩니다. 사용자가 형식화 미션을 시작하면, AI 에이전트가 그 미션을 향해 형식 증명을 기여하는 구조입니다.
Prove2Me가 제안하는 협업 구조
초록이 강조하는 핵심은 미션과 재사용입니다. Prove2Me에는 에이전트가 서로의 작업을 이어받고, 기존 결과를 자유롭게 재사용할 수 있도록 하는 메커니즘과 전용 하네스가 설계되어 있습니다.
이 구조가 중요한 이유는 분명합니다. 형식화 작업이 매번 처음부터 다시 시작된다면, 크라우드 소싱은 확장되기 어렵습니다. 반대로 이전 기여를 바탕으로 다음 기여가 자연스럽게 쌓인다면, 사람과 에이전트가 함께 더 큰 작업을 나눠 맡을 수 있습니다.
Prove2Me의 목표는 수학 형식화를 에이전트만 있으면 참여할 수 있는 확장 가능한 크라우드 소싱으로 만드는 것입니다.
여기서 말하는 참여 가능성은 전문가 자격을 없앤다는 뜻이 아니라, 형식화 기여의 문턱을 낮추려는 방향으로 읽는 것이 적절합니다. 초록 역시 장벽이 크게 줄었다고 말할 뿐, 전문성이 완전히 불필요하다고 주장하지는 않습니다.
올바름은 사람의 인상보다 기계 검사에 둡니다
Prove2Me의 또 다른 축은 검증 방식입니다. 초록은 사람과 에이전트가 협업하더라도, 최종적인 올바름은 기계가 검사한다고 분명히 말합니다.
이 점은 형식화 협업의 성격을 잘 보여 줍니다. 자연어로 미션을 설명하고 에이전트를 호출할 수는 있지만, 최종 산출물은 어디까지나 형식 증명이어야 합니다. 읽기에 그럴듯한 설명만으로는 완료를 판단할 수 없습니다.
형식화 협업의 신뢰는 사람의 리뷰만이 아니라 기계 검사를 통과하는 결과에서 나옵니다.
그래서 Prove2Me의 구상은 사람의 판단과 기계 검증을 분리하지 않습니다. 사람은 미션을 정의하고 방향을 잡으며, 에이전트는 형식 증명을 기여하고, 기계는 그 결과의 올바름을 검사하는 식입니다.
이 논문이 말하는 것과 말하지 않는 것
초록이 제시하는 범위를 분명히 보는 것도 중요합니다. 이 글은 플랫폼 설계와 목표를 소개하는 내용이지, 이미 확보된 대규모 운영 통계를 보고하는 글은 아닙니다.
따라서 초록에 없는 사용자 수, 증명 개수, 성공률 같은 숫자를 덧붙이면 원문을 벗어나게 됩니다. 마찬가지로, Lean 전문성이 전혀 필요 없다고 단정하거나, 사람 없이 자동으로 모든 형식화가 완성된다고 읽는 것도 과장입니다.
또한 이것은 특정 회사의 제품 출시 로드맵이 아니라 연구 논문과 개방 플랫폼 안내입니다. 모든 수학 분야가 즉시 형식화된다는 선언도 아닙니다. 초록이 말하는 것은 어디까지나 확장 가능한 크라우드 소싱을 지향하는 플랫폼의 구상입니다.
지금 이 플랫폼을 읽어볼 이유
Prove2Me가 흥미로운 이유는 Lean 4 자체의 기술적 진보만이 아니라, 형식화 작업을 협업 가능한 단위로 다시 설계하려 한다는 점에 있습니다. 한 사람이 긴 시간을 들여 끝까지 밀어붙이는 방식에서, 미션을 올리고 기여를 재사용하며 기계 검사를 통해 신뢰를 쌓는 방식으로 옮겨가려는 시도이기 때문입니다.
형식 검증이 더 넓은 참여를 얻으려면, 증명 자체만이 아니라 협업 구조도 함께 바뀌어야 합니다. Prove2Me는 바로 그 구조를 실험하는 플랫폼으로 읽을 수 있습니다.
참고 자료
arXiv:2608.28433
PDF
https://prove2.me
사람과 AI 에이전트가 함께하는 형식화 협업이 실제로 어디까지 확장될 수 있을지, 어떻게 보시는지 궁금합니다.