9월 6일 MIT 라이선스로 나온 MathKernel 은 SymPy·Z3·린(Lean)·CUDA 커널 같은 수학 엔진을 MCP 서버 하나로 묶고 계산마다 근거 등급을 붙여 돌려줘요. 등급은 린 커널이 받아들인 형식 증명서가 가장 위고 부동소수점 수치가 아래인데, 전체 신뢰도는 결론을 세우는 데 필요한 가장 약한 근거까지 내려가고 엔진끼리 답이 어긋나면 평균을 내지 않고 충돌 그대로 남겨요. 소수점이 하나라도 섞인 입력은 린 증명서와 Z3 반례를 아예 거부하는데 백엔드가 소수 표기를 정확한 분수로 바꿔 담아 다른 명제를 증명해 버리기 때문이라고 적어 뒀고, 저장소 자체는 9월 6일에 만들어져 커밋 11건에 별 49개예요.
용어 풀이
- MCP
- 에이전트를 외부 도구·데이터에 연결하는 표준 규약. Model Context Protocol.
- SymPy
- 식을 숫자로 계산하지 않고 기호 그대로 다루는 파이썬 수학 라이브러리.
- Z3
- 주어진 논리 조건을 만족하는 값이 있는지 기계로 판정하는 풀이기.
- 린(Lean)
- 증명을 기계가 검사할 수 있게 적는 정리 증명 언어이자 검사기.
- CUDA
- 엔비디아 그래픽 카드에서 계산을 돌리는 개발 환경.
운영자 인사이트
수학 전용이라 일반 코딩 작업에 붙일 자리는 좁고 저장소도 이틀밖에 안 됐지만, 도구가 돌려준 값에 근거 등급과 유래를 함께 싣고 약한 근거 쪽으로 신뢰도를 끌어내리는 설계는 에이전트가 도구 답을 그대로 사실로 받는 문제를 다루려는 MCP 서버라면 참고할 만해요. 다만 도구를 162개 여는 서버라 실제로 물릴 때는 도구 정의가 매 호출마다 실려 나가는 비용을 먼저 재 보세요.
여러 관점으로 보기
- 해커뉴스 반응 점수는 35점이고 댓글은 5건뿐인데, 그중 하나는 「AI 가 만든 티가 나지만 흥미로운 프로젝트」라면서도 「게임 없는 게임 엔진 같다」고 적었어요. Hacker News
- 완성도 판 번호는 1.3.0 인데 저장소는 9월 6일에 만들어져 커밋이 11건이고, 그중 한 건은 오픈AI 코덱스 계정이 쓴 것으로 남아 있어요. GitHub