Metamath 기반의 초심자 친화적 Proof Assistant, Starling 설계

Context

기존 Proof Assistant의 높은 진입 장벽으로 인한 초심자의 접근성 결여. 수학적 발견 과정에서 Computer-aided Proof의 중요성 증대 및 기존 도구의 복잡성 해결 필요성 대두.

Technical Solution

• Metamath를 Backend로 활용한 Surface Language 설계로 검증된 라이브러리와 Proof Verifier 상속
• JavaScript 기반 Compiler 구현을 통한 웹 환경 접근성 및 사용자 경험 개선
• Object Logics Agnosticism 특성을 유지하여 Quantum Logic 등 다양한 공리계 수용 구조 확보
• 복잡한 정형 검증 과정을 추상화한 User-friendly Interface 제공으로 학습 곡선 완화