Alok Singh

notational-fzf-vim. Notational velocity for vim.

rl_implementations. Reinforcement learning algorithm implementations and ML experimentation workspace

LeanPlot. Interactive React-powered charting library for Lean 4 in VS Code's infoview

python-conceal. Vim plugin for concise Python display using Unicode for subscripts and math notation

thread-twitter. Converts Twitter threads to Markdown files with proper reply indentation.

lean-inf. Levi-Civita field implementation in Lean 4 for computing with infinities and infinitesimals.

deep-rl-course. CS 294 (Deep Reinforcement Learning) at Berkeley

SEC-Edgar. Download all companies periodic reports, filings and forms from EDGAR database.

Limestone. Terminal-based data visualization library for Lean 4. Port of Granite (Haskell) with type-safe guarantees. Create beautiful charts using Unicode braille characters.

AsciiPlot. ASCII/Unicode plotting library for Lean 4 with legends and braille rendering

LeanTool. A "code intepreter" for Lean

infnum. Python library for infinite and infinitesimal numbers using Levi-Civita fields with PyTorch integration

ConvolutedProofs. Absurdly sophisticated proofs of simple mathematical facts in Lean 4

Hyperreals. Hyperreal number system implementation and formalization

lean-autograd. Automatic differentiation in Lean following JAX's autodidax tutorial

LeanDidax2. Pedagogical autodiff library in Lean 4 with forward/reverse modes and vectorization

MusicNotation. Pure functional music notation system in Lean 4 with Unicode visualization

NTSCDemodulator. Functional NTSC video signal demodulation in Lean 4

LeanHypothesis. Type-safe property-based testing for Lean 4 powered by Python's Hypothesis framework

Leantix. Lean 4 port of the Golitex typesetting system for LaTeX-like document processing

aoc_lean. Advent of Code 2023 solutions in Lean 4 with parser combinators

BasicSR. Basic Super-Resolution codes for development. Includes ESRGAN, SFT-GAN for training and testing.

llm.lean. Lean 4 transformer components with Karpathy's llm.c integration

RayTracingOneWeekend. Julia

ForAdem. Lean 4 project with LeanCopilot integration for AI-assisted theorem proving

graph-library-for-lean4. Graph algorithms and data structures for Lean 4 with performance benchmarks

FutureGAN. Official PyTorch Implementation of FutureGAN

first_and_last_word. Text scrambler preserving first and last letters to test readability claims

LeanPlusPlus. The increment operator in Lean 4

vim-gitignore. Gitignore plugin for Vim

skhd. Simple hotkey daemon for macOS

cartan_karlhede. Cartan-Karlhede algorithm for spacetime metric equivalence in Python and Lean 4

xai-hackathon. Personality analysis tool using Objective Personality Theory with Grok integration

IESRGAN. Improved ESRGAN

img-viz. Rust

deepul. Berkeley CS294-158 Deep Unsupervised Learning course materials and implementations

PermuteSum. Lean

rpn. Python

haskellBook. Haskell

Comonad. Port of Haskell comonad package to Lean 4 with store implementations

iron.nvim-1. Interactive Repl Over Neovim

LeanNetHack. NetHack DSL in Lean 4 with formal verification, AI algorithms, and ASCII visualization

TicTacToe. Fully-typed Tic-Tac-Toe in Lean 4 with DSLs for board literals and move scripts