-
tpil-solutions Public
My solutions to the exercises in "Theorem Proving in Lean 4"
-
knk-solutions Public
My solutions to the exercises in K. N. King's C programming book
-
lean-notes Public
A collection of my short Lean code for reference
-
talks Public
Slides used in my talks
Typst Creative Commons Attribution Share Alike 4.0 International UpdatedMay 2, 2025 -
batteries Public
Forked from leanprover-community/batteriesThe "batteries included" extended library for Lean 4
Lean Apache License 2.0 UpdatedApr 15, 2025 -
chzzk-custom-css Public
My custom CSS file for a Chzzk chat window
-
isprime Public
A Lean program that tests whether a natural number is prime
Lean Apache License 2.0 UpdatedApr 6, 2025 -
lean4 Public
Forked from leanprover/lean4Lean 4 programming language and theorem prover
Lean Apache License 2.0 UpdatedMar 27, 2025 -
lean4game Public
Forked from leanprover-community/lean4gameKorean translation of the Lean web game server
TypeScript GNU General Public License v3.0 UpdatedFeb 22, 2025 -
c-solutions Public
Forked from williamgherman/c-solutionsMy Solutions to K. N. King's "C Programming: A Modern Approach", second edition
C GNU General Public License v3.0 UpdatedFeb 6, 2025 -
theorem_proving_in_lean4 Public
Forked from leanprover/theorem_proving_in_lean4Theorem Proving in Lean 4 (fork of https://github.com/leanprover/theorem_proving_in_lean4)
JavaScript Apache License 2.0 UpdatedJan 30, 2025 -
NNG4 Public
Forked from leanprover-community/NNG4Korean translation of the Natural Number Game
Lean Apache License 2.0 UpdatedDec 13, 2024 -
doc-gen4 Public
Forked from leanprover/doc-gen4Document Generator for Lean 4
Lean Apache License 2.0 UpdatedDec 11, 2024 -
mm0 Public
Forked from digama0/mm0Metamath Zero specification language
Rust Creative Commons Zero v1.0 Universal UpdatedAug 23, 2024 -
SciLeanDemo Public
Forked from lecopivo/SciLeanDemoDemo project for SciLean
Lean UpdatedAug 21, 2024 -
SciLean Public
Forked from lecopivo/SciLeanScientific computing in Lean 4
Lean Apache License 2.0 UpdatedJun 5, 2024 -
-
LeanInk Public
Forked from leanprover/LeanInkLeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Lean Apache License 2.0 UpdatedMar 19, 2024 -
mathematics_in_lean_source Public
Forked from avigad/mathematics_in_lean_sourceSource code for the Mathematics in Lean tutorial.
Lean UpdatedMar 19, 2024 -
elan Public
Forked from leanprover/elanThe Lean version manager
Rust Apache License 2.0 UpdatedMar 19, 2024 -
elan-cleanup Public
Forked from JLimperg/elan-cleanupA tool for cleaning up unused Lean toolchains
Lean Apache License 2.0 UpdatedJan 18, 2024 -
SDL.lean Public
Forked from Anderssorby/SDL.leanSDL2 bindings for lean
Lean MIT License UpdatedJan 4, 2024 -
{{ message }}