Portable and lightweight brain segmentation in the terminal!

MoE training for Me and You and maybe other people

A free, open source, and extensible speech-to-text application that works completely offline.

An advanced keyboard manager

a lean4 type checker in idris2

Cuq: A MIR-to-Coq Framework Targeting PTX for Formal Semantics and Verified Translation of Rust GPU Kernels

Accelerated machine learning with dependent types

RealAnalysisGame

advent of code in idris2

A CLI tool for analyzing Claude Code/Codex CLI usage from local JSONL files.

Hardcaml is an OCaml library for designing hardware.

A purely functional programming language with first class types

A Full Live-Scripted CAD Kernel in the Browser

A markup-based typesetting system that is powerful and easy to learn.

Simple configuration and extra tools for NVIM + LSP + Idris2

LaTeX code for a paper on lean's type theory

Circuit IR Compilers and Tools

LLM inference in C/C++

Use your Mac trackpad as a weighing scale

get things from one computer to another, safely

Transforms complex documents like PDFs into LLM-ready markdown/JSON for your Agentic workflows.

Voice-to-text app for macOS to transcribe what you say to text almost instantly

A Lean companion to Analysis I

The open source coding agent.

Kimina Lean server (+ client SDK)

Natural Number Game

A Chrome extension that allows you to export your Claude.ai conversations in various formats (JSON, Markdown, Plain Text) with support for bulk exports and conversation browsing.