Projects — Jacob Reinhold

2026

lean-fmt site · code

Code formatter and linter for Lean 4, with editor and CI integration.
lean-lsp-plugin code

Native Lean 4 language-server integration for Claude Code.
lean-semantic-search code

Shared semantic-search foundation for Lean tooling.
lean-host-mcp code

MCP server hosting Lean 4 in-process.
lean-rs site · code

Rust bindings for hosting Lean 4.
sga site · code

English translation of the Grothendieck-era SGA seminars.
ega site · code

English translation of Grothendieck and Dieudonné's Éléments de Géométrie Algébrique.
mdwright site · code

Fast, configurable, math-aware Markdown linter and formatter.
lean-dup code

Duplicate detector for Lean.

uncertaintorcharchived paper · code

Uncertainty estimates for medical image synthesis and segmentation.
mssegarchived code

Multiple sclerosis T2 lesion segmentation.
counterfactualmsarchived paper · code

Counterfactual MR images of multiple sclerosis via structural causal models.

synthtorcharchived code

Deep-neural-network image translation and synthesis for MR images.
replicaarchived code

Synthesize MR brain images with a random forest.
intensity-normalization site · paper · code

Normalize the intensities of MR images.