Seiferas's simplified construction of the AKS O(log n) depth sorting network, formalised in Lean

A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions

A small cross-platform library for retrieving random data from (operating) system source

Verified computation of the Mandelbrot set Böttcher series

A formalized proof of Carleson's theorem in Lean

A simple raytracer written in Lean 4

Vim mode for VSCode, powered by Neovim

Formalizing stochastic doubly-efficient debate

The math library of Lean 4

Write C shims from within Lean code.

Library implementing type inference/checking functionality based on the Lean theorem prover

Lean 4 programming language and theorem prover

mold: A Modern Linker 🦠

High-level emulator for iPhone OS apps. This repo is used for issues, releases and CI. Submit patches at: https://review.gerrithub.io/admin/repos/touchHLE/touchHLE

A SwiftUI Mastodon client

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

Two-based indexing

ultrafast single TCP packet audio/visual experience

Minimal, type safe printf replacement library for C++

Extension for making GitHub great again

Fast Library for Approximate Nearest Neighbors

A massively parallel pentago solver

Source code for the version of pbrt described in the second edition of "Physically Based Rendering"

Fixed precision rational numbers exposed to python to test numpy user defined types

Numpy main repository

Investigations into simplified holdem poker

Combinatorial game theory exploration code

Miscellaneous very low priority ideas

An automated Bananagram player