Proposal of an LLM-Lean Approach and Architecture for Automated Mathematical Problem Solving

A Lean-facing multi-agent math-solving architecture where a falsifier makes the solver loop more inspectable and efficient.

A closed-agent architecture for mathematical problem solving that compares a Single solver structure with a Dual structure where a falsifier participates in the reasoning loop, emphasizing token/compute efficiency and final solving performance.

problem

LLM math solvers often produce plausible reasoning without a stable verification contract. For formal math workflows, the system needs a way to check, falsify, and iterate rather than only generate.

key idea

Compare a single solver structure with a dual closed-agent structure in which a falsifier participates in the reasoning loop and pushes the solver toward stronger final answers.

my role

Co-author; connected the Lean/AI4Math framing to the broader formalized mathematical-agent program.

methods

• Closed-agent solver/falsifier architecture
• Lean-oriented mathematical problem solving
• Token and compute efficiency comparison

evidence / results

• Recognized with a 2026 KIIS Spring Conference Best Paper Award
• Provides a public anchor for the IMDS Lean/AI4Math line

why this belongs in the portfolio

• Positions Lean as a working interface for mathematical agents
• Connects formal checking to agent workflow design

authors

Youngjik Lee, Jon-Lark Kim, Woo-Seok Jeong, Beom-Soo Kim, Jae-Hyun Baek

venue / status

2026 KIIS Spring Conference — Best Paper Award

Accepted conference paper and public institutional news item; source link available.