Coq-JR MCP server

// SPDX-License-Identifier: MPL-2.0 // SPDX-License-Identifier: CC-BY-SA-4.0

= Coq-Jr: Web-Native Interactive Theorem Proving image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"]

:toc: macro :toc-title: Contents :toclevels: 3 :icons: font :source-highlighter: rouge :experimental: :imagesdir: docs/images

[.lead] Coq-Jr is a lightweight, browser-native interface for the https://coq.inria.fr[Coq proof assistant], built with AffineScript. It provides HTTP and GraphQL access to interactive theorem proving, serving as both a standalone proof environment and a satellite component of the https://github.com/hyperpolymath/poly-proof-mcp[poly-proof-mcp] AI-accessible verification network.

[discrete] == Status: Alpha (v0.2.0-dev)

image:https://img.shields.io/badge/coq-compatible-orange[Coq Compatible] image:https://img.shields.io/badge/affinescript-v11-red[AffineScript] image:https://img.shields.io/badge/deno-v2-black[Deno]

'''

toc::[]

== What is Coq-Jr?

Coq-Jr democratizes formal verification by making the Coq proof assistant accessible through:

• Web Interface — An interactive browser-based IDE for writing and executing Coq proofs
• GraphQL API — Programmatic access for automated verification pipelines
• MCP Integration — AI-accessible proof assistance via the Model Context Protocol

Unlike traditional Coq installations requiring local setup, Coq-Jr runs entirely in the browser using WebAssembly, with optional server-side verification for enhanced capabilities.

=== Core Capabilities

[cols="1,3"] |=== |Feature |Description

|Interactive Proofs |Step through proofs with real-time goal display, tactic feedback, and error highlighting

|MathComp Support |Built-in Mathematical Components library for advanced mathematical reasoning

|Zero Installation |No local Coq installation required—proofs execute in WebAssembly

|Session Persistence |Save and resume proof sessions (roadmap)

|Multi-Backend |Pluggable architecture supporting jsCoq (browser) and SerAPI (server) backends |===

== The Hyperpolymath Ecosystem

Coq-Jr is one component of a larger formal verification ecosystem:

[source]

                ┌──────────────────────────────────────────────┐
                │           poly-proof-mcp                     │
                │    (AI-Accessible Proof Orchestration)       │
                └──────────────┬───────────────────────────────┘
                               │ MCP Protocol
       ┌───────────────────────┼───────────────────────┐
       │                       │                       │
       ▼                       ▼                       ▼
┌─────────────┐        ┌─────────────┐        ┌─────────────┐
│   Coq-Jr    │        │   ECHIDNA   │        │  Other      │
│  (Coq/Rocq) │        │ (12 provers)│        │  Provers    │
└─────────────┘        └─────────────┘        └─────────────┘
       │                       │
       │              ┌────────┴────────┐
       │              │                 │
       ▼              ▼                 ▼
┌─────────────┐ ┌───────────┐   ┌─────────────┐
│ echidnabot  │ │git-eco-bot│   │   ...       │
│(math verify)│ │(efficiency)│   │             │
└─────────────┘ └───────────┘   └─────────────┘

---

https://github.com/hyperpolymath/echidna[ECHIDNA]:: Neurosymbolic theorem proving platform supporting 12 proof assistants (Agda, Coq, Lean, Isabelle, Z3, etc.) with neural candidate generation

https://github.com/hyperpolymath/echidnabot[echidnabot]:: Mathematical verification bot for git forges—like Dependabot, but for proof obligations

https://github.com/hyperpolymath/git-eco-bot[git-eco-bot]:: Ecological and thermodynamic efficiency analysis for codebases

== Quick Start

=== Prerequisites

• https://deno.land[Deno] v2.0+
• https://nodejs.org[Node.js] v18+ (for AffineScript compilation only)

=== Installation

[source,bash]

Clone the repository

git clone https://github.com/hyperpolymath/coq-jr.git cd coq-jr

Install AffineScript compiler

npm install

Compile AffineScript sources

npm run res:build

Start the server

deno task dev

The proof environment is now available at http://localhost:8000

=== Docker (Coming Soon)

[source,bash]

docker run -p 8000:8000 ghcr.io/hyperpolymath/coq-jr:latest

== Usage

=== Web Interface

Navigate to http://localhost:8000 to access the interactive proof environment.

.Key Bindings [cols="1,2"] |=== |Key |Action

|kbd:[Alt+↓] / kbd:[Alt+N] |Execute next proof step

|kbd:[Alt+↑] / kbd:[Alt+P] |Undo last proof step

|kbd:[Alt+→] / kbd:[Alt+Enter] |Execute to cursor position

|kbd:[F8] |Toggle goal panel visibility |===

=== GraphQL API (Roadmap)

[source,graphql]

Start a new proof session

mutation { createSession(theorem: "forall n : nat, n + 0 = n") { sessionId goals } }

Execute a tactic

mutation { executeTactic(sessionId: "abc123", tactic: "intros n.") { goals proofState isComplete } }

Query available lemmas

query { searchLemmas(pattern: "comm", library: "mathcomp") { name statement library } }

=== MCP Integration (Roadmap)

For AI assistants using the Model Context Protocol:

[source,json]

{ "mcpServers": { "coq-jr": { "command": "deno", "args": ["run", "--allow-net", "mcp-server.mjs"], "env": { "COQ_JR_URL": "http://localhost:8000" } } } }

== Architecture

=== Technology Stack

[cols="1,1,2"] |=== |Layer |Technology |Purpose

|Frontend |AffineScript → JavaScript |Type-safe UI generation and DOM manipulation

|Server |Deno |HTTP server, static file serving, API endpoints

|Proof Engine |jsCoq (WebAssembly) |Browser-side Coq execution via WASM

|Styles |CSS |Custom styling with Bootstrap foundation |===

=== Module Structure

[source]

src/ ├── Main.res # Entry point and module exports ├── Page.res # HTML page generation ├── Components.res # Reusable UI components ├── JsCoq.res # jsCoq library bindings ├── Dom.res # Browser DOM API bindings ├── Server.res # HTTP server implementation └── Deno.res # Deno runtime bindings

=== Request Flow

[source]

Browser Request │ ▼ ┌─────────────────┐ │ Deno Server │ │ (Server.res) │ └────────┬────────┘ │ ┌────┴────┐ │ │ ▼ ▼ /index /static │ │ ▼ ▼ Page.res File I/O │ │ ▼ ▼ HTML Gen Asset │ │ └────┬────┘ │ ▼ HTTP Response │ ▼ ┌─────────────────────┐ │ Browser │ │ jsCoq (WASM) │ │ Proof Engine │ └─────────────────────┘

== Example: Infinitude of Primes

The default page demonstrates the classic proof that there are infinitely many primes:

[source,coq]

From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import eqtype ssrnat div prime.

Lemma prime_above m : {p | m < p & prime p}. Proof. have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0. exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m. by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1. Qed.

This proof uses the Mathematical Components library to show that for any natural number m, there exists a prime p greater than m.

== Development

=== Build Commands

[source,bash]

Watch mode for AffineScript compilation

npm run res:dev

Production build

npm run res:build

Start development server

deno task dev

Type check

deno check server.mjs

=== Testing (Roadmap)

[source,bash]

Run unit tests

deno test

Run integration tests

deno task test:integration

Run proof verification tests

deno task test:proofs

== API Reference

=== HTTP Endpoints

[cols="1,1,3"] |=== |Method |Path |Description

|GET |/ |Serve interactive proof environment

|GET |/index.html |Alias for /

|GET |/{file} |Serve static assets (CSS, JS, images)

|POST |/api/session (roadmap) |Create new proof session

|POST |/api/tactic (roadmap) |Execute tactic in session

|GET |/api/state/{id} (roadmap) |Retrieve proof state |===

=== Configuration

.Environment Variables [cols="1,1,2"] |=== |Variable |Default |Description

|PORT |8000 |HTTP server port

|COQ_PACKAGES |coq,mathcomp |Coq packages to load

|JSCOQ_CDN |unpkg |jsCoq distribution source |===

== Contributing

We welcome contributions! Please see link:.github/CONTRIBUTING.md[.github/CONTRIBUTING.md] for guidelines.

=== Development Philosophy

• Minimal dependencies — Prefer standard library solutions
• Type safety — Leverage AffineScript's type system
• Polyglot flexibility — Support multiple compilation targets (Deno, Node, browser)
• Accessibility — Theorem proving should be approachable

== License

Dual-licensed under your choice of:

• Palimpsest-MPL License v1.0 (PMPL-1.0)
• Palimpsest-MPL License v3.0 or later (MPL-2.0)

See link:LICENSE-PMPL-1.0[LICENSE-PMPL-1.0] and link:LICENSE-AGPL[LICENSE-AGPL] for details.

== Acknowledgements

• https://github.com/jscoq/jscoq[jsCoq] — The Coq proof assistant in the browser
• https://coq.inria.fr[Coq] — The formal proof management system
• https://math-comp.github.io[Mathematical Components] — A library for formalized mathematics
• The Hyperpolymath community for the broader verification ecosystem

---

[.text-center] Part of the https://github.com/hyperpolymath[Hyperpolymath] formal verification ecosystem