discussion_partner
Get proof strategy suggestions and alternative reasoning paths for Lean 4 code and math problems by querying Gemini or GPT models. Discuss approaches, compare suggestions, and debug stuck proofs.
Instructions
Use this tool to interact with a specialized partner model for proof strategies, reasoning, and formalization.
You can send Lean 4 code, natural language math problems, or proof strategies to different models
and get their suggestions. This is useful for:
- Discussing proof strategies and approaches
- Getting alternative reasoning paths
- Comparing suggestions from different models
- Debugging stuck proofs
Args:
question (str): Lean code, math problem, or any question you want to discuss.
model (str): Choose "gemini" (Google gemini-3-pro-preview) or "gpt" (OpenAI gpt-5.2-pro). Default is "gemini".
Returns:
str: The model's response.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| model | No | gemini | |
| question | Yes |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |