-
MusicNotation Public
Pure functional music notation system in Lean 4 with Unicode visualization
-
TetraGray Public
General-relativistic raytracer in Lean 4 with geometric algebra for black hole visualization
Lean UpdatedMar 30, 2025 -
NTSCDemodulator Public
Functional NTSC video signal demodulation in Lean 4
-
NameShadowingLinter Public
Linter to detect and warn about variable name shadowing in code
Lean Apache License 2.0 UpdatedMar 28, 2025 -
tyro Public
Forked from brentyi/tyroCLI interfaces & config objects, from types
Python MIT License UpdatedMar 27, 2025 -
cartan_karlhede Public
Cartan-Karlhede algorithm for spacetime metric equivalence in Python and Lean 4
-
LeanDidax2 Public
Pedagogical autodiff library in Lean 4 with forward/reverse modes and vectorization
-
Comonad Public
Port of Haskell comonad package to Lean 4 with store implementations
-
llm.lean Public
Forked from pimpale/llm.leanLean 4 transformer components with Karpathy's llm.c integration
-
voice_swap Public
Text-to-speech model with voice cloning and multilingual support using Zonos
Python UpdatedFeb 11, 2025 -
ddhodge Public
Forked from kazumits/ddhodgeModeling Latent Flow Structure using Hodge Decomposition
R Other UpdatedFeb 6, 2025 -
similar Public
Forked from mitsuhiko/similarA high level diffing library for rust based on diffs
Rust Apache License 2.0 UpdatedFeb 5, 2025 -
FPIL Public
Functional Programming in Lean book exercises with monad transformers
Lean UpdatedFeb 3, 2025 -
ARENA_3.0 Public
Forked from callummcdougall/ARENA_3.0Comprehensive ML curriculum: fundamentals, transformers, interpretability, RL, and LLM evaluations
Jupyter Notebook UpdatedFeb 3, 2025 -
LAsm Public
Functional assembly language written in Lean 4 with strong typing
Lean UpdatedFeb 1, 2025 -
AsciiPlot Public
ASCII/Unicode plotting library for Lean 4 with legends and braille rendering
-
SciLean Public
Forked from lecopivo/SciLeanScientific computing in Lean 4
Lean Apache License 2.0 UpdatedJan 28, 2025 -
LeanAide Public
Forked from siddhartha-gadgil/LeanAideTools based on AI for helping with Lean 4
Jupyter Notebook Apache License 2.0 UpdatedJan 21, 2025 -
ForAdem Public
Lean 4 project with LeanCopilot integration for AI-assisted theorem proving
-
Clifford Public
Lean 4 library for Clifford algebra (geometric algebra) and AI development testbed
UpdatedJan 9, 2025 -
lean-inf Public
Levi-Civita field implementation in Lean 4 for computing with infinities and infinitesimals.
-
LeanPlusPlus Public
The increment operator in Lean 4
-
posenc Public
Positional encoding experiments with rotations and complex representations
Python UpdatedDec 20, 2024 -
Bouyant Public
Port of Flocq floating-point formal verification library from Coq to Lean 4
Lean Apache License 2.0 UpdatedDec 10, 2024 -
bifunctors Public
Forked from ekmett/bifunctorsHaskell 98 bifunctors, bifoldables and bitraversables
Haskell Other UpdatedDec 9, 2024 -
aoc2024 Public
Lean 4 and AI-assisted solutions for Advent of Code 2024 challenges
Lean Other UpdatedDec 3, 2024 -
topgrade-1 Public
Forked from topgrade-rs/topgradeUpgrade all the things
Rust GNU General Public License v3.0 UpdatedNov 11, 2024 -
linear_canonical_transform Public
Mathematical transformations and signal processing in TeX
TeX UpdatedNov 11, 2024 -
-
xai-hackathon Public
Personality analysis tool using Objective Personality Theory with Grok integration
{{ message }}