우리는 이번 프리뷰 버전을 통해, 공식 정리 증명 분야에서 새로운 사고 기반 탐색 패러다임을 선도하는 대규모 언어 모델인 Kimina-Prover Preview를 소개한다. 이 모델은 Qwen2.5-72B를 기반으로 한 대규모 강화학습 파이프라인을 통해 훈련되었으며, 구조화된 사고 패턴인 \textit{공식적 사고 패턴}(formal reasoning pattern)을 활용하여 Lean 4에서의 증명 생성 성능이 뛰어나다. 이 접근 방식을 통해 모델은 인간의 문제 해결 전략을 모방하여 증명 단계를 반복적으로 생성하고 개선할 수 있다. Kimina-Prover는 miniF2F 벤치마크에서 기존 최고 성능을 초월하며, pass@8192 기준으로 80.7%의 성과를 기록했다. 벤치마크 성능 향상 외에도, 본 연구는 다음과 같은 핵심 통찰을 도출한다: (1) Kimina-Prover는 높은 샘플 효율성을 보이며, 최소한의 샘플링( pass@1) 조건에서도 우수한 성능을 발휘하고, 계산 자원의 규모에 따라 효과적으로 확장된다. 이는 모델의 독특한 사고 패턴과 강화학습 훈련 방식에서 기인한다; (2) 모델의 크기 증가에 따라 성능이 명확히 향상됨을 입증하였으며, 이는 이전까지 공식 수학 분야의 신경망 기반 정리 증명기에서 관찰되지 않았던 경향이다; (3) 기존의 전통적 탐색 알고리즘과는 차별화된 학습된 사고 방식은, 공식적 검증과 비공식적 수학적 직관 사이의 격차를 메울 잠재력을 보여준다. 본 연구는 Kimina-Prover의 소규모 버전(1.5B 및 7B 파라미터)을 오픈소스로 공개한다.