Wolfram Institute

Wolfram Language access to Lean’s mathlib for exact computation and machine-checked proofs

Wolfram Language interface for Lean 4 proof assistant

Build and publish a paclet's documentation, from markdown to a published paclet with its documentation site

A proof engine for the Calculus of Inductive Constructions, written in the Wolfram Language

GAPLink connects Wolfram Language to GAP.

Reference Lean environment for Rule 30 Prize submissions: the official statements, proved partial results and equivalent forms, and the verifier's checker

Geometry as effective description of large graphs

Convert literate markdown into Wolfram notebooks: documentation pages, resource definition notebooks, or plain notebooks, from a Template frontmatter key

Graph of graphs: Whitehead moves on cubic multigraphs, exact enumeration, field dynamics, and Wolfram notebooks.

A universal natural-number DSL for program synthesis and evolution, with lambda compilation and Lean-checked formal semantics.