Lean 로 작성된 라이브러리

lean4

Lean 4 프로그래밍 언어 및 정리 증명기.
  • 2.5k
  • Apache License 2.0

mathlib

Lean 수학적 구성 요소 라이브러리.
  • 1.6k
  • Apache License 2.0

smalltt

고성능 유형 이론 정교화를 위한 데모입니다.
  • 454
  • MIT

electrolysis

Lean 2(!)에서 기능 정제를 통해 Rust 프로그램을 간단하게 검증합니다.
  • 311
  • GNU General Public License v3.0

natural_number_game

Lean에서 자연수 만들기..
  • 272
  • Apache License 2.0

mathlib4

Lean 4를 위한 Mathlib 포트 작업이 진행 중입니다.
  • 261
  • Apache License 2.0

lean4-metaprogramming-book

  • 132
  • Apache License 2.0

lean-liquid

💧 액체 텐서 실험.
  • 128

lean4-raytracer

Lean 4로 작성된 간단한 레이트레이서.
  • 96
  • Apache License 2.0

logical_verification_2020

VU Amsterdam의 논리적 검증 2020–2021을 위한 동반 파일.
  • 96

hott3

Lean 3의 HoTT.
  • 71
  • Apache License 2.0

lean-chat

  • 46

Functional-Benchmarks

함수형 프로그래밍 언어 및 증명 도우미의 벤치마크 모음입니다.
  • 28

mathematica

MM-Lean 링크의 린 독립적 구현.
  • 24

BrouwerFixedPoint

  • 8

lamda_calculus_formalizations

  • 2
  • Apache License 2.0