[논문리뷰] PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean본 논문은 현대 연구 논문의 복잡한 증명 과정에서 발생하는 미세한 오류나 증명 격차(Gap) 문제를 해결하기 위해 PaperFormalizer를 제안한다. 기존의 수작업 검증은 시간이 과도하게 소요되며, 완전한 자동화 시스템은 자연어의 모호성이나 수정 방향에 대한 저자의 의도를 파악하지 못한다는 한계가 있다.#Review#Autoformalization#Lean#Agentic Pipeline#Author-in-the-Loop#Proof Assistant#LaTeX2026년 10월 25일댓글 수 로딩 중
[논문리뷰] MolLean: A Process-Verifiable Language for Chemical Reasoning본 논문은 기존 LLM 기반 화학적 추론이 구조적/속성적 환각(Hallucination)에 취약하며, 최종 답변의 정답 여부와 무관하게 추론 과정의 신뢰성이 낮다는 문제를 해결하고자 합니다.#Review#Chemical Reasoning#Process-Verifiable Language#Molecular State#Lean#Whole-Trace Refinement#MolLean-MCP2026년 10월 22일댓글 수 로딩 중
[논문리뷰] Lean Pool: An AI-Maintained Archive of Formalized Mathematics본 논문은 AI 시스템이 수학적 연구에 기여하는 속도가 인간의 이해 및 검증 속도를 초과함에 따라 발생하는 Formal Proof의 재활용 및 지속 가능성 문제를 해결하고자 Lean Pool을 제안한다.#Review#Formalized Mathematics#AI Agents#Lean#Mathlib#Archive#Proof Verification#Automated Maintenance#Compilation Optimization2026년 9월 22일댓글 수 로딩 중
[논문리뷰] Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction본 논문은 형식 증명 자동화(Automated Theorem Proving, ATP) 분야에서 기존의 대규모 모델 및 연산량 의존성을 극복하고, 더 적은 자원으로도 최첨단 성능을 달성하는 새로운 오픈소스 언어 모델 시리즈인 Goedel-Prover-V2 를 개발하는 것을 목표로 합니다.#Review#Automated Theorem Proving#Formal Verification#Language Models#Self-Correction#Data Synthesis#Reinforcement Learning#Model Averaging#Lean2025년 8월 6일댓글 수 로딩 중
[논문리뷰] Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving본 논문은 대규모 언어 모델(LLM)이 자연어 기반 정리 증명에서 명확한 감독 신호 부족으로 겪는 어려움을 해결하고자 합니다.#Review#Automated Theorem Proving#Large Language Models#Formal Verification#Reinforcement Learning#Lean#Geometry Reasoning#Chain-of-Thought#Lemma-Style Proving2025년 8월 2일댓글 수 로딩 중