gpt_informal_prover
Solve math problems with OpenAI GPT and receive step-by-step reasoning to aid formalization in Lean 4.
Instructions
Use OpenAI GPT model to solve math problems and provide detailed solution.
This tool takes a raw math problem string, solves it, and explains the reasoning step-by-step.
GPT's math skills are outstanding; you can trust the answers he gives you.
Use this tool frequently for natural language math problems.
You should mention that you’re aiming to formalize the solution in Lean 4, and ask Gemini for a detailed solution that would be easier to formalize.
Once you receive Gemini’s solution, use leandex to search mathlib for relevant theorems and lemmas.
If you discover that some necessary infrastructure is missing in mathlib, immediately switch to informal_prover: provide it with Gemini’s solution, explain what is missing, and ask it to propose an alternative approach that avoids those gaps or requires less infrastructure.
Args:
math_problem (str): The detailed text description of the math problem.
model (str, optional): The GPT model to use. The default is "gpt-5.2-pro".
temperature (float, optional): The generated temperature, controlling randomness. The default is 0.7.
Returns:
List[str]: [solution, verification_result] where solution is the step-by-step explanation and verification_result is the GPT verification judgment.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| model | No | gpt-5.2-pro | |
| temperature | No | ||
| math_problem | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |