alok

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

Berkeley, CA

Pinned Repositories

AsciiPlot
ASCII/Unicode plotting library for Lean 4 with legends and braille rendering
Language:Lean4 1 00
deep-rl-course
CS 294 (Deep Reinforcement Learning) at Berkeley
Language:Jupyter Notebook7 3 16
lean-inf
Levi-Civita field implementation in Lean 4 for computing with infinities and infinitesimals.
Language:Lean8 1 10
LeanPlot
Interactive React-powered charting library for Lean 4 in VS Code's infoview
Language:Lean90
LeanTool
A "code intepreter" for Lean
Language:Python41
notational-fzf-vim
Notational velocity for vim.
Language:Vim Script1.1k 12 6864
python-conceal
Vim plugin for concise Python display using Unicode for subscripts and math notation
Language:Vim Script17 3 14
rl_implementations
Reinforcement learning algorithm implementations and ML experimentation workspace
Language:Jupyter Notebook43 3 05
SEC-Edgar
Download all companies periodic reports, filings and forms from EDGAR database.
Language:Python6 5 00
thread-twitter
Converts Twitter threads to Markdown files with proper reply indentation.
Language:Python11 2 03

alok's Repositories

alok/LeanPlot
Interactive React-powered charting library for Lean 4 in VS Code's infoview
Language:Lean90
alok/LeanTool
A "code intepreter" for Lean
Language:Python41
alok/ConvolutedProofs
Absurdly sophisticated proofs of simple mathematical facts in Lean 4
Language:Lean2
alok/infnum
Python library for infinite and infinitesimal numbers using Levi-Civita fields with PyTorch integration
Language:HTML2 1 00
alok/Limestone
Terminal-based data visualization library for Lean 4. Port of Granite (Haskell) with type-safe guarantees. Create beautiful charts using Unicode braille characters.
Language:Lean1
alok/MusicNotation
Pure functional music notation system in Lean 4 with Unicode visualization
Language:Lean1
alok/NTSCDemodulator
Functional NTSC video signal demodulation in Lean 4
Language:Lean1
alok/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
alok/DocumentCalculus
Document Calculus formal system implementation in Lean 4 for document manipulation
alok/git-notifier
Email change notifications for git (and GitHub).
alok/Grassmann.jl
⟨Leibniz-Grassmann-Clifford⟩ differential geometric algebra / multivector simplicial complex
Language:Julia2 0
alok/import-graph
Tool to analyse the import structure of lean projects.
alok/lean4
Lean 4 programming language and theorem prover
Language:Lean0 0
alok/LeanBLAS
Bindings and specification for BLAS
alok/LeanHypothesis
Type-safe property-based testing for Lean 4 powered by Python's Hypothesis framework
Language:Lean
alok/LeanNetHack
NetHack DSL in Lean 4 with formal verification, AI algorithms, and ASCII visualization
Language:Lean
alok/LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
alok/Leantix
Lean 4 port of the Golitex typesetting system for LaTeX-like document processing
Language:Lean
alok/LeanYaml
YAML parsing and serialization library for Lean 4 with event-based processing
alok/libuv
Cross-platform asynchronous I/O
alok/llmvision
Visualize how LLMs tokenize text - see the world through the eyes of language models
Language:Python
alok/mathlib4
The math library of Lean 4
Language:Lean1 0
alok/modded-nanogpt
NanoGPT (124M) in 3 minutes
Language:Python
alok/modular-form-activation
PyTorch activation functions inspired by classical modular forms, featuring Dedekind eta function
Language:Python1 0
alok/PermuteSum
Language:Lean
alok/TetraGray
General-relativistic raytracer in Lean 4 with geometric algebra for black hole visualization
Language:Lean1 0
alok/TicTacToe
Fully-typed Tic-Tac-Toe in Lean 4 with DSLs for board literals and move scripts
Language:Lean
alok/UnusedPartial
A Lean 4 linter that detects unnecessary partial keywords in definitions
Language:Lean
alok/verso
Lean documentation authoring tool
alok/yaml
Support for serialising Haskell to and from Yaml.