Lemma Park가 코딩 에이전트로 수학 연구를 함께한다

Lemma Park에 참여한 코딩 에이전트가 수학 문제를 풀고 결과를 보고합니다. 저는 에이전트가 혼자 답을 내는 데 그치지 않고, 서로 결과를 이어 연구 경로를 찾는 구상이 눈에 남습니다. 한 번의 풀이 시연에서 멈추지 않고 공개 연구의 흐름을 만들려 하기 때문입니다.

Lemma Park의 에르되시 과제는 Lean으로 증명하는 작업입니다. Lean 4.35.0 소식은 프로젝트 증명을 점검하는 도구 개선을 다룹니다. 한쪽은 에이전트가 공개 수학 문제를 풀도록 모으고, 다른 쪽은 그 증명을 확인하는 환경을 넓힙니다.

개별 에이전트가 문제 하나를 푸는 데서 멈추지 않고, 참여자들이 공개 문제를 맡아 결과를 보고한 뒤 다음 경로를 찾습니다. 저는 풀이 능력만 보여주는 시연보다 연구 과정까지 함께 시험한다는 점이 반갑습니다.

성과 표시는 과제마다 차이가 큽니다. 에르되시 문제는 154개 중 1개가 증명된 반면, 소수 과제는 24개, 고전 정리 과제는 7개 모두 증명됐습니다. 과제별 난도가 같다는 정보가 없으니, 저는 이 수치를 하나의 전체 성적표로 묶지 않겠습니다. 사이트의 안전성 점검 100%와 검증 결과 69건도 서로 다른 지표입니다. 참여 명령은 내려받은 설치 스크립트를 바로 실행하므로, 안전 점검 수치가 개인의 실행 환경까지 안전하다고 보증하지는 않습니다.

참여를 고민하신다면 먼저 안내문과 설치 스크립트를 직접 읽고, 실행할 때는 개인 자료와 분리된 환경을 쓰십시오. 결과 목록에서 완료된 증명 하나를 열어 증명 내용과 검증 상태를 함께 확인해 보십시오. 둘이 확인되면 완료 집계의 근거를 살필 수 있고, 기록이 부족하면 활동 로그까지 대조해 보십시오.

코딩 에이전트가 낸 답을 마지막으로 검증 기록까지 따라가 본 것이 언제입니까?