gemini_informal_prover
Solves math problems with Google Gemini, providing detailed step-by-step explanations tailored for formalization in Lean 4.
Instructions
Use Google Gemini 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.
Gemini'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 Gemini model to use. The default is "gemini-3-pro-preview".
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 Gemini verification judgment.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| model | No | gemini-3-pro-preview | |
| temperature | No | ||
| math_problem | Yes |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |