litexlang/golitex

해결하는 문제

Litex는 자연스러운 수학적 기술과 형식적 검증 사이의 격차를 해결합니다. 기존의 증명 보조 도구는 수학자들이 실제로 문제를 해결하는 방식과 크게 다른 복잡한 타입 시스템 조율과 증명 스크립트를 배워야 하는 경우가 많습니다. Litex는 사용자가 수학적 사실을 자연스럽고 읽기 쉬운 순서로 기술할 수 있게 하면서, 기계는 루틴한 국소적 근거와 검증을 처리합니다.

작동 방식

Litex는 집합론 기반의 사실 중심 언어입니다. 수학적 객체, 정의, 사실의 검증된 컨텍스트를 유지함으로써 작동합니다.

• 사실 매칭: 시스템은 등가 대체, 정의, 그리고 양화된 규칙을 통해 루틴한 근거를 재구성합니다.
• 증명 프로세스: 복잡한 단계에 대해서는 사용자가 witness (존재 주장용), obtain (기존 증거 사용용), by contra (모순용), by induc (귀납용) 등의 명령어를 사용해 증명 경로를 명시적으로 정의할 수 있습니다.
• 검증: 수용된 모든 진술은 왜 수용되었는지(예: 특정 정의 또는 산술 규칙)와 미래 단계에서 사용 가능한 내용을 보여주는 증거를 제공합니다.
• Lean 통합: Litex는 중간 표현(IR)으로 컴파일할 수 있으며, 이 IR은 Lean 컴파일러에 의해 수용되어 Lean과 Mathlib의 캐리어 위에 의미적 래퍼를 생성합니다.

대상 사용자

• 수학자 및 학생: 전통적인 형식 언어의 급격한 학습 곡선 없이 익숙한 표기법으로 검증 가능한 수학을 작성하고 싶은 사람.
• AI 연구자: 기계 검증 가능한 국소 피드백과 명시적 가정을 필요로 하는 AI 수리 루프를 개발하는 개발자.
• 교육자: 현재 컨텍스트에서 특정 사실이 타당한지 즉각적으로 피드백을 제공하고 싶은 교사.

주요 특징

• 읽기 쉬운 구문: LaTeX 스타일 표기법과 집합론을 사용하여 코드를 일반적인 수학적 기술에 가깝게 유지합니다.
• 사실 중심: 증명 대체의 메커니즘을 수동으로 인코딩하는 대신 수학적 결론을 서술하는 데 초점을 맞춥니다.
• 검사 가능한 검증: 상세 진단(-detail 모드)을 제공하며, 개념과 정리 간의 연결을 시각화할 수 있는 관계 그래프를 생성할 수 있습니다.
• Lean 컴파일 경로: 고수준의 Litex 개발을 Lean 형식 언어로 변환할 수 있는 경로를 제공합니다.