This is your work, valued

Berkeley, CA

Alok Singh

Expert
@alok

If you’re a smooth operator, you can infinitely differentiate yourself.

notational-fzf-vim. Notational velocity for vim.

1.1k

rl_implementations. Reinforcement learning algorithm implementations and ML experimentation workspace

45

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

20

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

18

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

12

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

10

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

7

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

7

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

6

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

4

LeanTool. A "code intepreter" for Lean

4

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

4

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

3

Hyperreals. Hyperreal number system implementation and formalization

3

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

2

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

2

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

2

NTSCDemodulator. Functional NTSC video signal demodulation in Lean 4

2

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

2

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

2

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

1

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

1

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

1

RayTracingOneWeekend. Julia

1

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

1

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

1

FutureGAN. Official PyTorch Implementation of FutureGAN

1

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

1

LeanPlusPlus. The increment operator in Lean 4

1

vim-gitignore. Gitignore plugin for Vim

1

skhd. Simple hotkey daemon for macOS

1

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

1

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

1

IESRGAN. Improved ESRGAN

1

img-viz. Rust

1

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

1

PermuteSum. Lean

1

rpn. Python

1

haskellBook. Haskell

1

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

1

iron.nvim-1. Interactive Repl Over Neovim

1

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

1

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

1