Economics offers many theories that are highly useful in business. For example, the economic theory awarded the 2020 Nobel Prize in Economics (1) actually made a massive contribution to the design of spectrum allocation auctions in the United States, successfully creating a market worth over 100 billion dollars. Therefore, this time, I created a simple app using the mathematical proof program LEAN (2) to experiment and see if an AI agent using LEAN can be applied to economics. Let's get right into it.

1. Overview of the Developed App

Here is the app's screen. Because of my interest in building new markets, I named it the "Market Designs Verification App." It takes economic propositions and hypotheses and uses LEAN to automatically determine if there are any logical contradictions. I used Google Gemini 3.5 Flash for the natural language processing and Google ADK for the AI agent implementation. For the app development itself, I used Claude Code.

The proposition provided this time is as follows. It serves as an example of a simple business plan.

"I would like to report on the premise for goal setting for the next business plan. First, as for our current status, we have secured a solid baseline of at least 100 million yen in Annual Recurring Revenue (ARR). Building on this achievement, our policy for the next term is to set our target ARR at 1.7 times our current level (70% growth), aiming for further business expansion.
On the other hand, while pursuing growth, it is also necessary to develop a plan that takes into account the realistic constraints of the business environment. Considering the current framework of our internal budget and the limitations of our target market size, we do not intend to pursue an open-ended target ARR for the next term. Instead, we anticipate aiming for a realistic landing with a maximum cap of 150 million yen."

I want to verify this hypothesis using LEAN to confirm whether it is feasible. Of course, I want to avoid any hallucinations caused by the LLM.

2. Looking at the Analysis Report

When executing this app, the following report was generated in about 3 minutes. Let's take a look. First, the hypothesis, judgment, and conclusion are summarized. The bottom line is that the growth target exceeds the constraints, meaning execution is impossible.

The actual verification process using LEAN is displayed. It is a bit complex.

A DAG (Directed Acyclic Graph) is also used. In LEAN, once the compilation finishes, the verification is complete, meaning the proof has been established. Because it is executed strictly, the results are reliable. It is reassuring because there are no hallucinations like those seen with LLMs.

3. Implications Obtained

The implications obtained are as follows:

5. Economic Implication

The three business premises cannot all hold at once. To make the plan feasible, at least one premise must be relaxed. Concretely:

(a) Relax P1: lower the current-ARR floor 100 to ≤ 88.2353 (start from a smaller base).
(b) Relax P2: reduce the growth multiplier to ≤ 1.5× (keep multiplier × 100 ≤ 150).
(c) Relax P3: raise the target-ARR cap 150 to ≥ 170 (revisit budget / market-size constraints).

Based on these results, we must leverage them for business decision-making. This time, the results are well summarized, making them easy to understand. This is where the flexibility of LLMs comes into play. It is reassuring that if we can verify even complex management strategies with LEAN, we can automatically determine whether they can be executed without contradictions. In the future, this is expected to become an excellent advisor in boardroom meetings.

What did you think? It was a simple hypothesis verification, but I believe it is entirely possible to apply LEAN to economics. I felt that combining the flexibility of LLMs with the strictness of LEAN creates a wonderful system where they beautifully complement each other. I am looking forward to future developments. At Toshi Stats, we plan to continue tackling tasks in the field of economics using LLM + LEAN. Stay tuned!

You can enjoy our video news “ToshiStats AI Weekly Review” from this link, too!

1) Stanford Economists Paul Milgrom and Robert Wilson Win the Nobel in Economic Sciences, Stanford Graduate School of Business, Oct 12, 2020
2) LEAN

Notice: This is for educational purpose only. ToshiStats Co., Ltd. and I do not accept any responsibility or liability for loss or damage occasioned to any person or property through using materials, instructions, methods, algorithms or ideas contained herein, or acting or refraining from acting as a result of such use. ToshiStats Co., Ltd. and I expressly disclaim all implied warranties, including merchantability or fitness for any particular purpose. There will be no duty on ToshiStats Co., Ltd. and me to correct any errors or defects in the report, the codes and the software.

On June 3rd, a new research paper (1) was released by Google. It states that difficult mathematical proofs were solved by combining the LLM Gemini 3.1-pro with a mathematical proof language called LEAN (2). This time, I would like to delve into this paper and consider what kind of developments we can expect from this new AI agent in the future, beyond the framework of mathematics.

1. The Synergistic Effect of the LLM's Flexibility and LEAN's Strictness

Here is the paper, featuring an active AI agent called LEAP. It only uses Gemini 3.1-pro as the LLM, and no specific fine-tuning has been performed. It is being used straight out of the box. Even so, it is reported to demonstrate outstanding exploration capabilities in mathematical proofs. Since it doesn't require any particular additional training, it can be used immediately without doing anything, which is very convenient for practical use. Furthermore, by using LEAN in conjunction, if a proof with contradictory logic due to hallucinations is produced, an error occurs during compilation, creating a mechanism where it is automatically rejected.

LEAP (LLM-in-Lean Environment Agentic Prover)

Since LLM responses can fluctuate probabilistically, humans need to verify them in detail when conducting rigorous arguments. However, by introducing LEAN, this process has been automated. This is very reassuring. It seems that this fantastic result was achieved by combining the flexibility of the LLM and the strictness of LEAN in this way. Let's look closer.

2. The Structure and Accuracy of LEAP

Here is the structure of LEAP. The figure on the left is the roadmap for the theorem to be proved using LEAN. Technically, it forms a structure called a DAG (Directed Acyclic Graph). Complex mathematical proofs are not completed in a single attempt; the proof progresses by going back and forth between the LLM and LEAN several times. The key here is the section in the red frame, where the LLM describes an INFORMAL BLUEPRINT in natural language and converts it into a FORMAL SKETCH in LEAN. Furthermore, a two-tier review by LEAN and the LLM awaits. LEAN verifies whether the new proof method has any contradictions, and the LLM's review verifies whether that method is genuinely effective. In other words, the LLM acts as a pilot in the search for proof methods. Even though it's just using Gemini 3.1-pro as is, its potential is truly surprising.

Now, let's look at the results of applying LEAP to an actual task. It tackled the notoriously difficult Putnam 2025. Putnam 2025 contains twelve undergraduate-level problems from the 86th William Lowell Putnam Mathematical Competition, a highly challenging North American mathematics competition.

Looking at the DAG, you can see how the proof actually progresses. In this example of Putnam 2025 Problem A6, you can see layers upon layers of connected proofs. It's certainly a difficult problem. The green indicates the parts that have already been proven.

The results, as shown below, were that LEAP answered all questions correctly. An overwhelming accuracy.

You can see that while the original Gemini 3.1-pro couldn't score at all, it was able to demonstrate tremendous capabilities by combining it with LEAN. I think it is truly a breakthrough.

3. Beyond Mathematical Proofs into Various Fields

What we have seen so far were tasks related to mathematical proofs. With LEAP being able to construct such perfect logic, I felt it would be a waste to keep it confined solely to mathematics. In particular, its application to economics, which is directly linked to business practices, has immense scope and depth, and I believe it can contribute to expanding the areas where LLMs can be active. Economics is also generally described using mathematical formulas, so I think it has a high affinity with LEAP. A paper (3) on its application to economics has already been published, so if you are interested, please do give it a try.

What did you think? I believe the combination of LLMs and LEAN will be expanded and improved in various ways in the future. It might be stepping closer to AGI. It's very exciting.

At Toshi Stats, we plan to take on tasks in the field of economics moving forward. Stay tuned!