-
-
analysis Public
Forked from teorth/analysisA Lean companion to Analysis I
Lean Apache License 2.0 UpdatedOct 28, 2025 -
nanochat Public
Forked from karpathy/nanochatThe best ChatGPT that $100 can buy.
Python UpdatedOct 13, 2025 -
Limestone Public
Terminal-based data visualization library for Lean 4. Port of Granite (Haskell) with type-safe guarantees. Create beautiful charts using Unicode braille characters.
-
-
libuv Public
Forked from libuv/libuvCross-platform asynchronous I/O
C MIT License UpdatedAug 1, 2025 -
lean4 Public
Forked from leanprover/lean4Lean 4 programming language and theorem prover
Lean Apache License 2.0 UpdatedJul 31, 2025 -
LeanPlot Public
Interactive React-powered charting library for Lean 4 in VS Code's infoview
-
git-notifier Public
Forked from rsmmr/git-notifierEmail change notifications for git (and GitHub).
Python Other UpdatedJul 26, 2025 -
ConvolutedProofs Public
Absurdly sophisticated proofs of simple mathematical facts in Lean 4
-
llmvision Public
Visualize how LLMs tokenize text - see the world through the eyes of language models
Python MIT License UpdatedJul 26, 2025 -
LeanTool Public
Forked from GasStationManager/LeanToolA "code intepreter" for Lean
-
TicTacToe Public
Fully-typed Tic-Tac-Toe in Lean 4 with DSLs for board literals and move scripts
Lean MIT License UpdatedJul 1, 2025 -
UnusedPartial Public
A Lean 4 linter that detects unnecessary partial keywords in definitions
Lean MIT License UpdatedJun 21, 2025 -
LeanNetHack Public
NetHack DSL in Lean 4 with formal verification, AI algorithms, and ASCII visualization
Lean UpdatedJun 20, 2025 -
Leantix Public
Lean 4 port of the Golitex typesetting system for LaTeX-like document processing
Lean UpdatedJun 13, 2025 -
mathlib4 Public
Forked from leanprover-community/mathlib4The math library of Lean 4
Lean Apache License 2.0 UpdatedJun 13, 2025 -
LeanBLAS Public
Forked from lecopivo/LeanBLASBindings and specification for BLAS
Lean Apache License 2.0 UpdatedJun 13, 2025 -
yaml Public
Forked from snoyberg/yamlSupport for serialising Haskell to and from Yaml.
Haskell UpdatedJun 12, 2025 -
LeanYaml Public
YAML parsing and serialization library for Lean 4 with event-based processing
UpdatedJun 12, 2025 -
LeanHypothesis Public
Type-safe property-based testing for Lean 4 powered by Python's Hypothesis framework
Lean UpdatedJun 11, 2025 -
verso Public
Forked from leanprover/versoLean documentation authoring tool
Lean Apache License 2.0 UpdatedMay 22, 2025 -
modular-form-activation Public
PyTorch activation functions inspired by classical modular forms, featuring Dedekind eta function
Python UpdatedMay 22, 2025 -
modded-nanogpt Public
Forked from KellerJordan/modded-nanogptNanoGPT (124M) in 3 minutes
Python MIT License UpdatedMay 16, 2025 -
infnum Public
Python library for infinite and infinitesimal numbers using Levi-Civita fields with PyTorch integration
-
DocumentCalculus Public
Document Calculus formal system implementation in Lean 4 for document manipulation
UpdatedMay 12, 2025 -
LeanSearchClient Public
Forked from leanprover-community/LeanSearchClientSyntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
Lean Apache License 2.0 UpdatedApr 30, 2025 -
batteries Public
Forked from leanprover-community/batteriesThe "batteries included" extended library for the Lean programming language and theorem prover
Lean Apache License 2.0 UpdatedApr 30, 2025 -
import-graph Public
Forked from leanprover-community/import-graphTool to analyse the import structure of lean projects.
Lean Apache License 2.0 UpdatedApr 30, 2025 -
Grassmann.jl Public
Forked from chakravala/Grassmann.jl⟨Leibniz-Grassmann-Clifford⟩ differential geometric algebra / multivector simplicial complex
Julia GNU Affero General Public License v3.0 UpdatedApr 28, 2025
{{ message }}