[G1-Sync] Manual knowledge update

10_Wiki/Topics/Automated-Theorem-Proving.md

@@ -1,5 +1,5 @@
 ---
-id: P-REINFORCE-AI-THEOREM
+id: [[P-Reinforce]]-AI-THEOREM
 category: "10_Wiki/💡 Topics/AI"
 confidence_score: 0.94
 tags: [Theorem Proving, Coq, Lean, Formal Verification]
@@ -12,10 +12,10 @@ last_reinforced: 2026-04-20
 > "코드가 맞다"고 믿는 것이 아니라, 수학적으로 "틀릴 수 없음"을 컴퓨터가 강제로 증명하게 만드는 소프트웨어 신뢰성의 정점이다.
 
 ## 📖 구조화된 지식 (Synthesized Content)
-- **Hilbert's Program & Decidability**:
+- **Hil[[BERT]]'s Program & Decidability**:
     - 모든 수학적 명제를 기계적으로 판별할 수 있는지에 대한 질문에서 시작되었다. 비록 불완전성 정리에 의해 한계가 밝혀졌으나, 특정 영역에서의 자동 증명은 비약적으로 발전했다.
 - **Formal Verification (형식 검증)**:
-    - 운영체제 커널(seL4)이나 금융 스마트 컨트랙트처럼 단 하나의 버그도 허용되지 않는 곳에서, 프로그램이 사양(Specification)대로 동작함을 논리적으로 입증한다.
+    - 운영체제 커널(seL4)이나 금융 스마트 컨트랙트처럼 단 하나의 버그도 허용되지 않는 곳에서, 프로그램이 사양([[Specification]])대로 동작함을 논리적으로 입증한다.
 - **Lean & Coq (Proof Assistants)**:
     - 최근 AI(LLM)와 결합하여 인간이 수학 문제를 풀 듯 증명 과정을 생성하고 검증하는 '대화형 증명 도우미'가 대세다.