leannode-core

A minimal Node.js wrapper for the Lean 4 theorem prover.

Installation

npm install leannode-core

Prerequisites: You must have Lean 4 installed and available in your PATH.

Usage

const LeanRunner = require('leannode-core');

// Basic evaluation
const result = await LeanRunner.run('#eval 2 + 3');
console.log(result.stdout); // "5"

// Define and evaluate
const code = `
def factorial : Nat → Nat
| 0 => 1  
| n + 1 => (n + 1) * factorial n

#eval factorial 5
`;

const result = await LeanRunner.run(code);
console.log(result.stdout); // "120"

API

LeanRunner.run(leanCode, options?)

Executes Lean code and returns a promise with the result.

Parameters:

• leanCode (string): The Lean code to execute
• options (object, optional):
  • args (array): Additional command line arguments for Lean
  • cwd (string): Working directory for the Lean process
  • env (object): Environment variables

Returns: Promise resolving to:

{
  stdout: string,  // Standard output from Lean
  stderr: string,  // Standard error from Lean  
  exitCode: number // Process exit code (0 = success)
}

Testing

npm test

License

MIT