Euler-Theorem-Prover

Euler Theorem Prover is a child-friendly Prolog and web theorem prover that derives closed forms for sums by using Euler-style integration, Euler-Maclaurin correction terms, polynomial expansion, and symbolic simplification. Unlike the Gaussian Theorem Prover, which discovers formulas through pattern tables and Gaussian elimination, this system explains sums as areas, curves, staircases, endpoint corrections, and symbolic integration.

Stage 1 implementation

Stage 1 includes:

• Core project structure with Prolog modules under prolog/
• Main proving predicate prove/2
• Support for:
  • sum(i,1,n,i)
  • sum(i,1,n,i^2)
  • sum(i,1,n,i^3)
  • sum(i,1,n,(i+2)^2)
  • sum(i,1,n,i^3 + 0.5)
  • sum(i,1,n,3*i^2 + 2*i + 1)
• Algorithm aliases (for example algorithm(sum_squares))
• Child explanation and diagram descriptors
• Basic browser demo (index.html, app.js)

Stage 2 implementation

Stage 2 adds:

• prove_algorithm/3 for extracting closed form and proof steps directly
• Algorithm method variants:
  • integration approximation
  • known formula expansion
  • Euler-Maclaurin
  • split polynomial terms
  • compare methods
• Extended polynomial support in Euler summation up to degree 5 terms
• Stage 2 web demo behavior with method-aware output text

Stage 3 implementation

Stage 3 adds:

• Flexible web-text parsing for sum <var> from <start> to <end> of <expr> inputs
• Method-specific proof-step tails for algorithm modes, including compare-methods steps
• Stage 3 tests for web-text parsing, compare-method algorithm flow, and web_output/2 projection

Stage 4 implementation

Stage 4 adds:

• Stage 4 web_output/2 formatting with method labels and string-based proof/diagram lines for JSON-like web projection
• Explicit input field in projected web output for stable web payload shape
• Stage 4 tests for output-shape and method-label behavior

Stage 5 implementation

Stage 5 adds:

• Child-friendly diagram text projection in web_output/2 for staircase, curve, endpoint correction, and split-term views
• Method-aware child explanation lines for compare-methods, known-formula, split-term, and integration-approximation flows
• Stage 5 tests for descriptive diagram output and compare-method child explanation text

Stage 6 implementation

Stage 6 adds:

• Explicit integration-based pipeline steps in euler_pipeline/2 (prove_each_term_by_euler, combine_term_proofs, and output packaging)
• Per-term Euler proving flow before combining and verifying the final closed form
• Stage 6 tests validating split-term term proving and method-specific algorithm proof steps

Stage 7 implementation

Stage 7 adds:

• Explicit symbolic integration rule coverage in integration.pl for variable, powers, constants, sum/difference, and scalar multiples
• Stage 7 PL-Unit tests validating the required integration rules from pr2.txt
• Stage 7 test wiring in both npm test and tests/run_tests.pl

Stage 8 implementation

Stage 8 adds:

• Simplified Euler-Maclaurin coverage checks for required polynomial sums through degree 5
• Canonical closed-form simplification for subtraction terms in Euler polynomial formulas
• Stage 8 tests validating all required examples from the Euler-Maclaurin requirements section

Stage 9 implementation

Stage 9 adds:

• Explicit alternative-algorithm mode checks for integration, known-formula, Euler-Maclaurin, and split-terms square-sum strategies
• Validation that all Stage 9 algorithm variants produce the same square-sum closed form
• Validation that prove_algorithm/2 returns method, closed form, proof steps, and child explanation for algorithm mode

Stage 11 implementation

Stage 11 adds:

• Web-interface coverage tests for the required input box, method dropdown, prove button, and output sections
• Validation that the required method options are present in the web dropdown
• Validation that app.js wires prove-button actions into closed-form, proof-step, child-explanation, and diagram outputs

Stage 12 implementation

Stage 12 adds:

• Child-friendly visualisation wording aligned with staircase, smooth-curve/integral area, and endpoint-correction descriptions
• Stage 12 tests that validate required diagram descriptors and web output visual lines
• Web demo diagram output strings updated from internal identifiers to human-readable diagram descriptions

Stage 14 implementation

Stage 14 adds:

• README description text aligned with the required Stage 14 wording in pr2.txt
• Stage 14 tests that verify both required README description sentences are present

Stage 15 implementation

Stage 15 adds:

• Stage 15 tests for the GitHub-agent prompt requirements in pr2.txt
• Validation of required supported sum inputs and algorithm-style proving input
• Validation that theorem output includes closed form, proof steps, child explanation, web-ready output projection, and required module presence

Run tests

npm test

(Requires SWI-Prolog / swipl in your environment.)

Quick Prolog usage

?- [prolog/main].
?- prove(sum(i,1,n,(i+2)^2), Result).