Research — PKBoost AI Labs | Mar 2025 – Present

LEMMA is a research prototype demonstrating scalable hybrid reasoning for automated theorem proving. It reproduces Google DeepMind’s 2024 AlphaProof approach, combining Monte Carlo Tree Search (MCTS) with a Transformer policy network.

Key Features

  • Formal Verification: 450+ formally verified transformation rules spanning algebra, calculus, and number theory.
  • No Hallucination: Provides proof traces with complete step-by-step justification.
  • Hybrid Architecture: Custom AST parser, MCTS with UCB selection, and a Transformer policy network (Candle).
  • Synthetic Training: End-to-end pipeline generating 17,000 synthetic problems for policy network training.

Results

  • Accuracy: 95.2% on single-step problems, 100% on multi-step problems (31-test benchmark).
  • Scale: 47k Lines of Code (Rust).

Links: GitHub | License: Mozilla Public License 2.0