Lean To Code Translator W Proof - C Rust Wasm by Apoth3osis

Name: Lean To Code Translator W Proof - C Rust Wasm
Brand: Apoth3osis
SKU: 69cdb31aff055c86b8b8a224
Price: 0.05 USD
Availability: InStock

Lean To Code Translator W Proof - C Rust Wasm

Available ActionsEach successful request consumes credits as outlined below.

generate^5crverify^5crget_targets^5crget_task^5crlist_tasks^5cr

Details

The Lean to Code Translator converts exportable Lean proof programs into auditable C, Rust, or WebAssembly deliverables. Upload a Lean source bundle, choose the entry module and symbol, and get generated code plus a certificate, logs, and a verification bundle so you can preserve provenance, re-run validation, and confirm the artifact still matches the original source under the pinned runtime.

Use Cases

Compile Lean proof programs to C for native integration, Generate Rust exports from pinned Lean proof bundles, Produce constrained Wasm artifacts from Lean proof code, Package code generation runs with certificates and logs, Verify previously generated bundles before shipping or publication, Preserve reproducible build evidence for audits and reviews, Archive proof export bundles for downstream teams

Connect Your Agent In 5 Min

Watch the setup guide for your platform

Or Install Locally

STDIO connector for Claude Code, Codex, Cursor, Zed, and other LLMs that require STDIO or custom connections. This lightweight connector routes requests to https://api.agentpmt.com/mcp. All tool execution happens in the cloud and the server cannot edit any files on your computer.

npm install -g @agentpmt/mcp-routeragentpmt-setup

Actions(5)

generate^5cr6 params

Compile a source-only Lean archive into verified C, Rust, or Wasm artifacts using the platform-pinned runtime and shared cache. This action starts an asynchronous task and returns a task_id immediately.

source_archive_file_idstring

Stored zip archive containing Lean source files under UserProofs/. Do not upload lakefile.lean, lean-toolchain, lake-manifest.json, or .lake.

use_vendored_runtimeboolean

When true, generate from the vendored Lean runtime shipped in the isolated lean-service container.

entry_modulestring

Lean module to import from the uploaded source tree, for example UserProofs.Main.

entry_symbolstring

Lean definition to export from entry_module. Fully qualified names are accepted; unqualified names are tried as bare names and common namespace-qualified forms.

target_languagestring

Target language to generate. Supported values: c, rust, wasm.

Values:

crustwasm

timeout_secondsinteger

How long to wait for the isolated lean-service request before failing.

Range: 10 - 300

verify^5cr4 params(1 required)

Verify a previously generated Lean proof export bundle against the same pinned runtime and shared cache. This action starts an asynchronous task and returns a task_id immediately.

bundle_file_idrequiredstring

Stored bundle zip file_id produced by a previous generate call.

target_languagestring

Target language encoded in the bundle. Supported values: c, rust, wasm.

Values:

crustwasm

verification_modestring

Use fast for hash checks or full to rebuild and re-export.

Values:

fastfull

timeout_secondsinteger

How long to wait for the isolated lean-service request before failing.

Range: 10 - 300

get_targets^5cr0 params

List the currently supported target languages and bundle requirements.

No parameters for this action.

get_task^5cr1 param(1 required)

Check the status of a generate or verify task and retrieve results when complete.

task_idrequiredstring

Task ID returned from a previous generate or verify call.

list_tasks^5cr1 param

List recent generate and verify tasks for the current budget.

limitinteger

Maximum number of tasks to return. Default 20.

Range: 1 - 100

curl -X POST "https://api.agentpmt.com/products/purchase" \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer ********" \
  -d '{
    "product_id": "69cdb31aff055c86b8b8a224",
    "parameters": {
      "action": "generate"
    }
  }'

import requests
import json

url = "https://api.agentpmt.com/products/purchase"

headers = {
    "Content-Type": "application/json",
    "Authorization": "Bearer ********"
}

data = {
    "product_id": "69cdb31aff055c86b8b8a224",
    "parameters": {
        "action": "generate"
    }
}

response = requests.post(url, headers=headers, json=data)
print(response.status_code)
print(response.json())

const url = "https://api.agentpmt.com/products/purchase";

const headers = {
  "Content-Type": "application/json",
  "Authorization": "Bearer ********"
};

const data = {
  product_id: "69cdb31aff055c86b8b8a224",
  parameters: {
    "action": "generate"
  }
};

fetch(url, {
  method: "POST",
  headers: headers,
  body: JSON.stringify(data)
})
  .then(response => response.json())
  .then(data => console.log(data))
  .catch(error => console.error("Error:", error));

const axios = require('axios');

const url = "https://api.agentpmt.com/products/purchase";

const headers = {
  "Content-Type": "application/json",
  "Authorization": "Bearer ********"
};

const data = {
  product_id: "69cdb31aff055c86b8b8a224",
  parameters: {
    "action": "generate"
  }
};

axios.post(url, data, { headers })
  .then(response => {
    console.log(response.status);
    console.log(response.data);
  })
  .catch(error => {
    console.error("Error:", error.message);
  });

Login to view your API and budget keys. The example above uses placeholder values. Sign in to see personalized code with your bearer token.

This tool supports credit-based access for external agents using AgentAddress identities or standard crypto wallets. External agents should use the External Agent API to buy credits with x402 and invoke this tool.

1. Buy Credits

Purchase credits via x402 payment (500 credit minimum, 100 credits = $1).

# Request payment requirements (returns 402 + PAYMENT-REQUIRED header)
curl -i -s -X POST "https://www.agentpmt.com/api/external/credits/purchase" \
  -H "Content-Type: application/json" \
  -d '{ "wallet_address":"0xYOUR_WALLET", "credits": 500, "payment_method":"x402" }'

# Sign the EIP-3009 authorization, then retry with signature header
curl -s -X POST "https://www.agentpmt.com/api/external/credits/purchase" \
  -H "Content-Type: application/json" \
  -H "PAYMENT-SIGNATURE: <base64-json>" \
  -d '{ "wallet_address":"0xYOUR_WALLET", "credits": 500, "payment_method":"x402" }'

2. Create a Session Nonce (nonce used in signed balance/invoke)

curl -s -X POST "https://www.agentpmt.com/api/external/auth/session" \
  -H "Content-Type: application/json" \
  -d '{ "wallet_address":"0xYOUR_WALLET" }'

3. Invoke This Tool

Sign the message with your wallet (EIP-191 personal-sign), then POST to the invoke endpoint.

# Sign this message (wallet MUST be lowercased):
# agentpmt-external
# wallet:0xyourwallet...
# session:<session_nonce>
# request:<request_id>
# action:invoke
# product:69cdb31aff055c86b8b8a224
# payload:<sha256(canonical_json(parameters))>

curl -s -X POST "https://www.agentpmt.com/api/external/tools/69cdb31aff055c86b8b8a224/invoke" \
  -H "Content-Type: application/json" \
  -d '{
    "wallet_address": "0xYOUR_WALLET",
    "session_nonce": "<session_nonce>",
    "request_id": "invoke-uuid",
    "signature": "0x<signature>",
    "parameters": {
      "action": "your_action",
      "your_param": "value"
    }
  }'

Compile Lean proofs into auditable code artifacts

Proof Code Compiler starts asynchronous Lean proof export and verification jobs that produce reproducible C, Rust, or WebAssembly artifacts plus the files needed to audit and verify them later.

Read the full Lean input tutorial or download the working example zip.

Async workflow

Call generate or verify. The tool returns a task_id immediately.
Poll get_task with that task ID.
When the task reaches completed, read the result payload for artifact metadata and file IDs.
Use list_tasks to review recent jobs for the current budget.

What to upload for generation

Upload a .zip with a top-level UserProofs/ directory that contains only Lean source files.

user_source.zip

└── UserProofs/

├── Main.lean

├── Helpers.lean

└── Submodule/Util.lean

Do not upload lakefile.lean, lean-toolchain, lake-manifest.json, or .lake/. The platform supplies the pinned Lean toolchain and runtime.

Generate inputs

source_archive_file_id
entry_module, such as UserProofs.Main
entry_symbol, such as exportProgram
target_language: c, rust, or wasm

You may also set use_vendored_runtime for the built-in smoke-test program or adjust timeout_seconds within 10-300 seconds.

Verification inputs

Use the bundle_file_id from a completed generation task. Choose fast to re-check hashes and certificate details, or full to rebuild and compare regenerated output under the pinned runtime.

Task results

Completed tasks can return generated output metadata, a verification bundle, a certificate, a generation log, and normalized source-archive metadata. Keep the bundle file ID if you want to verify the export later.

About The Developer

Apoth3osis

★15 stars

Joined Agent Payment: August 14, 2025

We build tools that enable AI agents to excel in the mathematical realm.

Our small team develops experimental and unique solutions in the AI arena, with a strong focus on modular computing for agentic applications and custom model deployment. We have handled projects for a variety of applications across many sectors, from algorithmic trading and financial analysis, to molecular simulations and predictions, to habitat and biodiversity monitoring and wildlife conservation.

Frequently Asked Questions

Can I upload `lakefile.lean`, `lean-toolchain`, or my own build configuration?

No. The platform pins the Lean toolchain and exporter runtime for you. Do not include `lakefile.lean`, `lean-toolchain`, `lake-manifest.json`, or `.lake/` in the uploaded archive.

Does this compile any Lean program?

No. The selected definition must elaborate to `HeytingLean.LeanCP.CProgramDecl`, which is the exportable LeanCP program form supported by the current compiler path.

What do `entry_module` and `entry_symbol` mean?

`entry_module` is the Lean module imported from your uploaded source tree, such as `UserProofs.Main`. `entry_symbol` is the definition exported from that module, such as `exportProgram`.

What do I upload to Proof Code Compiler?

Upload a `.zip` whose top-level folder is `UserProofs/` and whose contents are Lean source files only. A single-file project can be as small as `UserProofs/Main.lean`.

What is the difference between `fast` and `full` verification?

`fast` checks certificate details and hashes without rebuilding. `full` rebuilds and re-exports under the pinned runtime, then compares the regenerated output with the stored artifact for stronger assurance.

What should I save after a successful generation?

Save the generated output file, the certificate, the generation log, and especially `artifacts.bundle.file_id`. The bundle is what you need for later verification.

Which target should I choose?

Use `c` when you want the broadest and lowest-risk support. Use `rust` when you want the same export path with Rust output. Use `wasm` only when you are comfortable with the current target being more constrained than `c`.

Lean To Code Translator W Proof - C Rust Wasm

Description