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.