nesy-solver

Public proof playground at nesy-solver.dev — submit proof obligations, get prover recommendations, stream verdicts back live.

Table of Contents

• Overview
• Supported Formalisms
• Architecture
• License

Overview

nesy-solver is the interactive frontend for the hyperpolymath neurosymbolic learning loop. It connects users directly to the Hypatia + Echidna + VeriSim pipeline:

1. Submit a proof obligation in SMT-LIB, Lean 4, Coq/Rocq, Idris2, or Agda

2. The app recommends a prover strategy based on live proof_attempts data in VeriSim

3. Dispatches to Echidna for execution

4. Streams the verdict back in real time

5. Records the attempt in verisim-api — the playground improves its recommendations over time from actual usage data

Supported Formalisms

• SMT-LIB (Z3, CVC5)

• Lean 4

• Coq / Rocq

• Idris2

• Agda

Architecture

Component	Role
web/	Frontend (ReScript + Deno)
src/core/	Proof dispatch and strategy selection
src/interface/abi/	Idris2 ABI for prover interface contracts
src/interface/ffi/	Zig FFI bridge to Echidna + external provers
deploy/	Container deployment (Containerfile, Podman)
verisim-api	External: records proof attempts, drives strategy recommendations

License

MPL-2.0. See LICENSE.