Slavomir Kaslev

torch-spherical-harmonics. Real Spherical Harmonics for PyTorch

Cells2Pixels. Jupyter Notebook

JaxProof. Lean

brax. Massively parallel rigidbody physics simulation on accelerator hardware.

ptxmemorymodel. Coq

localsend. An open-source cross-platform alternative to AirDrop

Naturality. F. William Lawvere, Andrée Ehresmann, and Grothendieck

flappy. A flappy bird clone in Lean

uring-trace. Visualization tool for your IO-uring workload

Slug. Reference code for the Slug Algorithm.

slug-webgpu. WebGPU implementation of Eric Lengyel's Slug algorithm for resolution-independent vector text rendering on the GPU

ffc.h. Single-header c99 accelerated float/double parsing. Port of the fast_float library.

unique_id. C++

Bitmap. Lean 4 bitmap utilities with PNG encode/decode support, plus a small widget for visualization.

brotli. Brotli compression format

veil. A verifier for automated and interactive proofs about transition systems.

moss-kernel. Rust Linux-compatible kernel

SlidingHardwareEstimator. C++

series. Power series arithmetic in Lean

brownian-motion. Construction of a Brownian Motion in Lean

xemu. Original Xbox Emulator for Windows, macOS, and Linux (Active Development)

path_tracer. An educational path tracer written in C using Vulkan to supplement a lecture series on path tracing.

MinecraftHDL. A Verilog synthesis flow for Minecraft redstone circuits

catlang. an arrowized category-forward language

zig-time-sharing-kernel. Minimal implementation of a time-sharing kernel on RISC-V, implemented in Zig, on top of OpenSBI

narya. A proof assistant for higher-dimensional type theory

strongpnt. Lean

colmap. COLMAP - Structure-from-Motion and Multi-View Stereo

black_hole. Black hole simulation project:

gpt-oss. gpt-oss-120b and gpt-oss-20b are two open-weight language models by OpenAI

dragonbox. Reference implementation of Dragonbox in C++

quic. In-kernel QUIC implementation with Userspace handshake

rbtree. A simple, intrusive, zero-allocation red-black tree implementation

ebtree. Elastic Binary Trees

cebtree. Compact Elastic Binary Trees: only require two pointers, like a doubly-linked list, to build a tree. Duplicates not implemented for now, but algorithmically supported.

pogocache. Fast caching software with a focus on low latency and cpu efficiency.

physarum-36p. physarum/organic simulation in openFrameworks, inspired by 36 Points

tcp-in-udp. Lightweight TCP in UDP tunnel 🚇 using eBPF 🐝

cartier. Rocq Prover

monoid_homology_stuff. Miscellaneous tools about semigroups and their homology

beagle. Beagle - git-compatible revision control for modern workflows 🐕 (The repo was split, see https://github.com/gritzko/beagle-ext)

c2rust. Migrate C code to Rust

sequencelib. A platform for formalizing OEIS sequences in Lean 4

formal-conjectures. A collection of formalized statements of conjectures in Lean.

webgpu-raytracer. A software raytracing engine written in WebGPU

scylla. Scylla, a tool for translating ultra-regular C code to Safe Rust

c4. C in four functions

rusty_chip. Rust

raddebugger. A native, user-mode, multi-process, graphical debugger.

cubecl. Multi-platform high-performance compute language extension for Rust.

hashtable-benchmarks. Jupyter Notebook

FiniteStateEntropy. New generation entropy codecs : Finite State Entropy and Huff0

gol.py. efficient Game of Life in Python

libqsbr. QSBR and EBR library

junction. Concurrent data structures in C++

funtrace. A fast, small C/C++ function call tracer for x86-64/Linux, supports clang & gcc, ftrace, threads, exceptions & shared libraries

tinybvh. Single-header dependency-free BVH construction and traversal library.

snake. A 54 bytes snake game in x86 assembly

tt08-vga-donut. Verilog

FindMy.py. 🍏 + 🎯 + 🐍 = Query Apple's FindMy Network with Python!

StringZilla. Up to 100x faster strings for C, C++, CUDA, Python, Rust, Swift, JS, & Go, leveraging NEON, AVX2, AVX-512, SVE, GPGPU, & SWAR to accelerate search, hashing, sorting, edit distances, sketches, and memory ops 🦖

libusual. Modern C Environment

QRception. C

sketches. A Haskell blog

dspbr-pt. A WebGL2 Enterprise PBR sample renderer

Babylon.js. Babylon.js is a powerful, beautiful, simple, and open game and rendering engine packed into a friendly JavaScript framework.

blink. tiniest x86-64-linux emulator

nsync. nsync is a C library that exports various synchronization primitives, such as mutexes

regex-deriv-reproving-agda-in-lean. Symbolic and Automatic Differentiation of Languages in Lean

seek-tune. An implementation of Shazam's song recognition algorithm.

grothendieck.

zenphoton. The "Zen photon garden", an HTML5 raytracing art-toy.

MaterialEggs.

Co-dfns. High-performance, Reliable, and Parallel APL

ATmega328P-watering-system. A small and efficient home plant watering system.

Coq-BB5. Rocq Prover

blis. BLAS-like Library Instantiation Software Framework

version2. Vector class library, latest version

HoTTLean. Lean

Poly. A Lean4 Formalization of Polynomial Functors

warp. A Python framework for GPU-accelerated simulation, robotics, and machine learning.

OpenPBR. Specification and reference implementation for the OpenPBR Surface shading model

ThunderKittens. Tile primitives for speedy kernels

lean-derived-categories. Formalization of derived categories in Lean/mathlib

homotopy-rs. A Rust/WASM implementation of homotopy.io

EulerProducts. An attempt at formalizing facts on Euler products in Lean

jax. Composable transformations of Python+NumPy programs: differentiate, vectorize, JIT to GPU/TPU, and more

rzk. An experimental proof assistant based on a type theory for synthetic ∞-categories.

globular. Globular

notes-on-realizability. Lecture notes on realizability

shady. Research shading language IR

co-tracker. CoTracker is a model for tracking any point (pixel) on a video.

ooj. the origins of J

atree. Stevan Apter-style trees in C++17

LeanCopilot. LLMs as Copilots for Theorem Proving in Lean

Foundation. Formalization of Mathematical Logic

sh-lib. Spherical/zonal harmonics library

lean4lean. Lean 4 kernel / 'external checker' written in Lean 4

exponential-ramsey. A formal proof of an exponentially better upper bound on Ramsey numbers

pfr. Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

jeri. Javascript Extended Range Imaging Viewer

ray. Formalizing results about the Mandelbrot set in Lean

symmetric_project. Lean

pulsar. A modular and blazing fast runtime security tool for the IoT, powered by eBPF.

TypeTopology. Logical manifestations of topological concepts, and other things, via the univalent point of view.

hapi. The Simple, Secure Framework Developers Trust

solid. A declarative, efficient, and flexible JavaScript library for building user interfaces.

O1ShufflingGrouping. The code to accompany "Constant Time Stateless Shuffling and Grouping"

usehooks. A collection of modern, server-safe React hooks – from the ui.dev team

lean4. Lean 4 programming language and theorem prover

SciLean. Scientific computing in Lean 4

TS1. Lean

Meshroom. Node-based Visual Programming Toolbox

TaskMatrix. Python

gitea. Git with a cup of tea! Painless self-hosted all-in-one software development service, including Git hosting, code review, team collaboration, package registry and CI/CD

goflow2. High performance sFlow/IPFIX/NetFlow Collector

ruff. An extremely fast Python linter and code formatter, written in Rust.

entt. Gaming meets modern C++ - a fast and reliable entity component system (ECS) and much more

cam-combi. Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

graph-force. Python library for embedding large graphs in 2D space, using force-directed layouts.

tcc-lean-alg-geom-2022. Experiments in algebraic geometry as part of the EPSRC Taught Course Centre course on formalising number theory and geometry

go-shellwords. Parse line as shell words

server. Robb Oat is a robot software engineer.

tinygrad. You like pytorch? You like micrograd? You love tinygrad! ❤️

lean4-samples. Code samples for Lean 4

heroku-free-alternatives. Free tier of Heroku Dynos, Postgres and Data for Redis will no longer be available after November 28, 2022. Let's find a list of services with a free plan that developers can use as an alternative to Heroku. Feel free to submit PRs and improve the list.

Swift_OpenGL_Example. :star: Swift OpenGL Example written in swift (for Ubuntu, macOS, iOS and Android)

scott. Selected Papers of Dana S. Scott

helix. A post-modern modal text editor.

icu4x. Solving i18n for client-side and resource-constrained environments.

uaamg. C++

Bringing-Old-Photos-Back-to-Life. Bringing Old Photo Back to Life (CVPR 2020 oral)

lean4-balance-car. Lean4 port of Arduino balance car controller

lean4-maze. maze game encoded in Lean 4 syntax

lean-snakebird. An implementation of Snakebird in Lean.

awesome-cold-showers. For when people get too hyped up about things

rvm-find. Relevance Vector Machines (RVMs) for Bayesian data-driven discovery of PDEs.

Stockfish. A free and strong UCI chess engine

squarefree_asymptotics. A formally verified proof that the density of squarefree numbers is ζ(x)⁻¹

LabCamera. A physically based camera model for virtual production and computer graphics

wfc. Wave Function Collapse library in C, plus a command-line tool

drgn. Programmable debugger

hms. Hilton-Milnor splitting

complex_time_integrators. This repository contains code to explore the unique properties of complex time integration.

orleans. Cloud Native application framework for .NET

Nuklear. A single-header ANSI C immediate mode cross-platform GUI library

btop. A monitor of resources

template. This is the repository for the distill web framework

qasync. Python library for using asyncio in Qt-based applications.

py2many. Transpiler of Python to many other languages

freemocap. Free Motion Capture for Everyone 💀✨

lean4-papyrus. An LLVM interface for Lean 4. (WIP)

formalising-mathematics. Lean 3 material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

wg-manager. A easy to use WireGuard dashboard and management tool

SDF. Collection of resources (papers, links, discussions, shadertoys,...) related to Signed Distance Field

lean-gptf. Interactive neural theorem proving in Lean

Analytic. lecture notes for Analytic Geometry course

topos. Topos theory in lean

tiny-cuda-nn. Lightning fast C++/CUDA neural network framework

traversable-fincontainer. Coq

libsnark. C++ library for zkSNARKs

fourier-feature-networks. Fourier Features Let Networks Learn High Frequency Functions in Low Dimensional Domains

series-formelles. Translation of, and commentary on, Joyal's classic paper "Une théorie combinatoire des séries formelles" (A combinatorial theory of formal series)

tfhe. TFHE: Fast Fully Homomorphic Encryption Library over the Torus

Matlab-simulation-of-Schramm-Loewner-Evolution. Description and analysis of some mathematical/physics phenomena by using simulation

ganja.js. :triangular_ruler: Javascript Geometric Algebra Generator for Javascript, c++, c#, rust, python. (with operator overloading and algebraic literals) -

c-iterators. :books: A demonstration of implementing a "type-safe" lazy iterator interface in pure C99

pyzx. Python library for quantum circuit rewriting and optimisation using the ZX-calculus

idris2dart. The Dart backend for Idris 2.

compute_rasterizer. Rendering Point Clouds with Compute Shaders

AdvancedHMC.jl. Robust, modular and efficient implementation of advanced Hamiltonian Monte Carlo algorithms

usdmanager. USD Manager

vampire. The Vampire Theorem Prover

lawvere. The collected works of F. W. Lawvere

helpers. some small helper tools

RamanujanMachine. Python

datatype99. Algebraic data types for C99

fiat-crypto. Cryptographic Primitive Code Generation by Fiat

fract. Jupyter Notebook

xg2xg. by ex-googlers, for ex-googlers - a lookup table of similar tech & services

boltzmann-brain. Analytic sampler compiler for combinatorial systems

buntdb. BuntDB is an embeddable, in-memory key/value database for Go with custom indexing and geospatial support

linuxdeployqt. Makes Linux applications self-contained by copying in the libraries and plugins that the application uses, and optionally generates an AppImage. Can be used for Qt and other applications

Chronos. Chronos - A static race detector for the go language

LLFF. Code release for Local Light Field Fusion at SIGGRAPH 2019

nerf. Code release for NeRF (Neural Radiance Fields)

practical-path-guiding. Code of "Practical Path Guiding for Efficient Light-Transport Simulation"

nanogui. Minimalistic C++/Python GUI library for OpenGL, GLES2/3, Metal, and WebAssembly/WebGL

tev. High dynamic range (HDR) image viewer for people who care about colors

raspi3-tutorial. Bare metal Raspberry Pi 3 tutorials

threadx. Eclipse ThreadX is an advanced real-time operating system (RTOS) designed specifically for deeply embedded applications.

vs-chromium. A Visual Studio extension containing a collection of tools to help contributing code to the Chromium project.

DAIN. Depth-Aware Video Frame Interpolation (CVPR 2019)

rcu_cell. rust rcu cell library

geode. A computational geometry library for C++ and Python

soa-derive. Array of Struct to Struct of Array helpers in Rust

Intuitive-Guide-to-Maxwells-Equations. An intuitive and visual guide to understanding Maxwell's equations.

tymly. An open framework for building digital services.

jo. Jo - Java way to do Ko

accelerate-examples. Examples for the Accelerate language