RT optimization

1hr -> 10min

v0.6: 3 Infra — Check

Incubator

Verifier

External Checker + HTML bug fixes.

Theory Compressor

v0.4 — Compressor + HTML Proof Graph
Compressor
Post-proof theorem set minimization. Announced externally as “Pruner,” renamed to Compressor internally to avoid ambiguity with the Pick-and-Prune algorithm central to the prover.
Tests each theorem for redundancy: if it can be re-derived from the remaining set, it is eliminated. Two phases — dependency discovery via independent Logic Blocks, then greedy elimination sorted by redundancy.
Results: Peano 64→17 theorems (73%), Gauss 20→12 (40%). Adds ~1s to a 407s pipeline.
HTML Proof Graph Visualization
Navigable HTML proof graph with chapter-based structure, theorem cross-referencing, and full derivation provenance. Extensive debugging pass covering variable renaming, anchor resolution, and proof origin handling.
A fully verified version will follow once the proof graph verifier is integrated.​​​​​​​​​​​​​​​​

v0.3

feat(gl): introduce integration for compound logical structures; derive Gauss summation formula (rt: 6 min)

Performance update for Peano

• feat(core): rewrite prover in C++17 (MSVC 2022), batched CE filtering, unify to single “full run” mode — 5h → 7s and 4 GB → 1 GB peak.

Summary

Prover rewritten in modern C++17 and built with MSVC 2022. Execution is parallelized across all logical cores on a single machine.

Counterexample (CE) filtering added.

Runtime and memory improved substantially.

Measured impact (Dell G16 7630, release x64)

Prover runtime: ~5 hours → ~7 seconds.

Peak memory (RSS): ≈ 1 GB during CE filtering.

User-visible changes

Only one run mode remains: full run. (Quick/almost full removed.)

Default execution uses all logical cores; CE filter batch size scales with core count.

Generative Logic v0.1

First public release of Generative Logic.