AGI, Spring 2026, Homework 2
Prof. Iddo Drori, last updated 2/8/26


In this homework you will use AI agents to prove and verify a small open math or theoretical CS problem.


1. Installation and setup:
Install Anthropic's Claude Code, OpenAI's Codex app, and the free student version of Google's Gemini-3 Pro
Update Claude Code to the latest version (by claude update in the command line) and use Opus 4.6, and update Codex app to the latest version
Ask Claude Code to "enable agent teams" (in Claude Code), see https://code.claude.com/docs/en/agent-teams#use-case-examples
Ask Claude Code to install an open source Claude Code Lean agent prover, such as https://github.com/project-numina/numina-lean-agent, will install Lean (~5GB)
Choose a small open problem in natural language to work on, save it as problem.txt


2. Proof in natural language:
Ask GPT-5.2 Pro Extended thinking to prove the problem using the prompt below
GPT will answer, ending with open sub-problems and optionally suggest “If you want, I can…”
Respond “yes / you choose, and work on the open sub-problems.", and continue this iteratively 
until GPT-5.2 Pro responds that the problem is solved, and save the entire concatenated conversation into a proof.txt file.
Ask GPT-5.2 Extended thinking to write the entire solution it found so it is correct and complete and ready for review and is in precise natural language before autoformalization into Lean, and save the proof.txt file.
Share your GPT link, for example (S10,S9,S5,S2,S1):
https://chatgpt.com/share/6986c290-9fbc-8012-8937-c78187a7adba
https://chatgpt.com/share/6986c2c9-6974-8012-b418-43f1a29326b0
https://chatgpt.com/share/6986fc9f-cd9c-8012-a02b-897ba9abd914
https://chatgpt.com/share/69876b09-5604-8012-bef5-ec52564effc1
https://chatgpt.com/share/6986ba36-8fbc-8012-adfc-777fabf13fa9

Prompt:

Problem Solver

Problem
{problemText}
{commentsText}

Instructions

You are solving an open problem. These are unsolved problems — most have resisted expert attacks. A rigorous partial result or a well-documented failure is more valuable than a fake proof.

What to do

1. Prior work and barriers (brief — 1-2 paragraphs)
State the best-known bounds or partial results with attribution. Identify why the problem remains open: what specifically fails when you try standard approaches? If you recognize the problem, say what is known. Do NOT pad this section with textbook definitions.

2. Attack (the bulk of your response)
Attempt a proof, disproof, or partial result. Requirements:

* Number all major logical steps (Step 1, Step 2, …).
* Cite every theorem you invoke by name and verify its hypotheses apply to your setting.
* If a step requires an unproven claim, mark it with  and state it as a conditional: “If X holds, then…”
* If you reach an impasse, document exactly where and why the argument breaks. Then try an alternative approach. Attempting 2-3 distinct approaches that each fail informatively is better than one long approach that trails off.
* If you cannot improve on known results, say so explicitly. Do not repackage known bounds as new results.

3. Verification
Before finalizing, re-examine your argument adversarially:

* For each key step, ask: Would a skeptical referee accept this? Is any implication actually an equivalence? Are quantifiers in the right order?
* Check: do boundary cases (n=1, 2, 3) or degenerate cases break the argument?
* Check: Did you use any theorem whose hypotheses you did not verify?
* Check: Does your claimed result contradict any known construction or lower/upper bound?
* If you find an error, fix it or downgrade your claim. Do not leave a known error in the final output.

Common failure modes to avoid

* Survey masquerading as progress: Summarizing known results without contributing anything new. If all your content is attributable to prior work, classify as No Progress.
* Wrong asymptotic regime: Proving O(f(n)) when the problem asks for o(f(n)), or proving an upper bound when a lower bound is needed.
* Unverified theorem application: Invoking a theorem (Szemerédi Regularity, Hales-Jewett, etc.) without checking that your objects satisfy its hypotheses.
* Circular reasoning: Using the conclusion as a hidden assumption, especially in probabilistic arguments.
* Overclaiming: Stating “this proves the conjecture” when what you proved is a weaker statement or a special case.

Output Format

Prior Work

[Best known results, key references by author name, and why the problem is open.]

Approach

[Which strategy do you choose and why. If multiple approaches were attempted, describe each.]

Solution / Analysis

[The complete mathematical argument with numbered steps. If partial, clearly state what is proved vs. what remains open. Mark conditional steps with .]

Verification

[Your self-check. For each key deduction, state whether it survives scrutiny. If you found and fixed errors, document them.]

Result

* Status: [Solved / Major Partial Result / Minor Partial Result / Documented Failure / No Progress]
* What is proved: [One sentence stating your strongest unconditional result, or “No new result beyond known bounds.”]
* Open sub-problems: [If applicable, specific sub-problems whose resolution would complete the proof.]


3. Proof formally verified in Lean:
Do a Lean game https://adam.math.hhu.de/#/g/leanprover-community/nng4
Use https://live.lean-lang.org to check that a simple Lean program compiles.

Copy problem.txt and proof.txt to a project directory; in Codex app add a new project; start Claude Code from the project directory.

Prompt Codex 5.3 Extra High to use the Lean installation available in the prover agent directory, installed earlier.

a. Problem in Lean using the Codex app:
Prompt Codex 5.3 Extra High to only formalize the problem in Lean 4, verify that the problem in Lean compiles, provide the Lean problem file problem.lean, then remove the comments from the Lean problem file, next backtranslate the Lean 4 problem into natural language problem.lean-nl.txt, and finally check if the original problem.txt and the backtranslated Lean in natural language problem.lean-nl.txt are mathematically equivalent, and provide the problem.lean, problem.lean-nl.txt, and check result.

b. Proof in Lean using the Codex app:
Prompt Codex 5.3 Extra High to formalize the natural language proof.txt into a Lean 4 proof proof.lean, without sorry statements or axioms, that:
i. Compiles (proof.lean)
ii. When the comments are removed from the Lean proof file and the Lean proof is backtranslated to natural language (proof.lean-nl.txt)
should be mathematically equivalent to the original proof.txt.
Prompt Codex to use the installed Lean or https://live.lean-lang.org to verify that the proof compiles, for example (P10,P9,P5,P2,P1):

https://live.lean-lang.org/#codez=PQWghAUAKgFglgZwAQDM4BsCmTGoK7roCeSAxgPYB2CALgE56k1wBu2AFJeUgA7oCGpTDHLoAJpjoIAlADoIAQUJJMADxqTK/dEkp4AtpLiltIfluIJc/BAgM9mVZPzrZMlChLFIbK1X2M4GiRaBiY8Vwg0THEEYBgiHnIaGEwENIAaH0pvbR0JOlZMb1c7dBpnV146cjZvCmp6RmY2YnkQYAgILUMEHkFsAAUARgAGLrxKIqlsPC7QMCQAYiWkBQAjUMFg9DhKTBcQch5JfhpyOhxKDToUAaQOrtDmiOwAGT2DugB5HmQAd1SkSQSAAsmckAAuJAAOQhgCTCWEIpBQRKzCAggBqmFIUKRwURqJOSDmILYuOhAG9KEhLtC4TQAL5IRHg4I0y6I7G4zhIABUtOkGKQ+gIoMxeMp+l0eIZzNZEOlNK5OJlKtx+nm4GWq1B5AkIAA1khdvsXCEiLRMNL+qRDfwAOZ7B0PToQZ7hKp6iQAaQAypaNNL2MdkNCPmafn9pEheXT8THAZJMMKFMc8aHZGyZZykJnsxzhets9D8xDCyCFBm/lmIbyBXQY/XBUXqwhZNzYzSG0KyTiAPppnhQ4UgwAAREgABpt2vs2kZUcgvM18mxodTmMAXkXS+X7dF6HFselkM3Mp7XahZ+7grWsczq8nvaQ5P76xnq+LELP6y6EhQSB+qIbAIL8pznJclKhniEZfL8CDMtStKymcjKLuwfp4t6mD+oG1p7jmTYAOozgWt7QoMNTDqewp+rI64kWedFfjQf6YABQHoCB3IQXAABexRIFBfwwZ8LjwYhHIoUy6GYdC2G4Va0rQRyxGkeW5FIJR6Y0SCmYHke7Ante/K3ryp7nredFViGK6qkRW6AbIv4QCkmAXPh5K8QJYj9uQKB+ScdBnBc/YIKIeCOJQi7CWGSCweJfySch9KobJWH6jhAZKQRqmxiRpY1mRjboTABWAcBaRgcFEGAUgDkjrunHcTi3mCZhBU/kQwpiFY+jDgA2s1VVBSFdBZMNCA8Rc/HFAAuj4wRlUggBFRMKJjoKQi76WKEpGVelmNpeFk3kd1n3nZuINWeD6qhh9Hpg1FnrN1u4gn1/QklYlAuvdr4MXICBEPomq7v2SA3ZdTksQdL0hHA/VIANZVzYu4NMc5B10a+LluR5ymjRBfkBV5M0+WFEVRTF0HhmJUYIUJUmpTJu4YRlvrZUGuVmeVZZziVrMwNyACSlAAFZ4hOlLTgAmup/OMlkt24tOkPtqucuIqrSAy8+ILsMt0KTdNhQ+XVT2LpN1VjebsOvUgvUI4NVuExcE2VVNrVk/Ni1IMta0gmo2x+yL4uxi9i4bVtb17rIq73QDEM7m9O2HntxmHU2NInaZZ30Rd6v2TGukx05/2Pcn6PQwdZWVxDsersxJYYzjshAyDQquak+PLuBoVwCgJNe6bxQU+gkVwFQ1MibTkYSYzKX4mhrNyWCmWKVzKk8/LhGlaHEvQlLss7xyisN6q2vKzrLJTvXuuNUuLt95cHVIIAKYQVVxaQm7N3iv899sGgeggsKAA7X4YOpMR6+X8oFZ+Y8J5UHNmAiBTBe41VCrAqBv8EFRVtkLHEosxZakWCsMEZxCiqBACgVw2BtAOhmikG0gh7ROh+q6J4TRPTYDZJQgAYrQpQDDChMILqJOe0ZLzxgZImIEKYQT8B4HwEghV2zFRvnzHMwo6AwDipoisPglHEDCicCkSAJzTlUbOHMWRFHKNvmeOxxApzaN0SY1U0IdHIDPF4rUIAIDCwAuYHw6BhFBBgNKXAfQcQDzgIJc4ZByD9UitgAABkOVJ2RvCpJYqkrIQQcDIAoHQVwaCUAXCQG5EUmUjQWiUu0ToeNXDSn0BQuAqgBGYEwP2ehjCIn9mKaU1iu5YriLgklBe0i0or3ZllPCBNkCqXQkIrCbSOmCNCX0hZu9BYKCMSo8xt8rHFSyEI2QTiSDa2sumJ8pUABKui8RnK8fXJuZxi7oQsSfecaxQnnP2Q435DpZAvI/k/DBL8Nx22FHseg3BJw9Q+kjcFY1UYgiAVwkBIJwGwpqH7IRkdtDRzetc4c2szkXKOV1C0IMADcqClp7PsQimOVdnmPIsjAAlrLXnOWbn7B5CAUG4u4DAP0hLNrJwpQCq5D0yU1yZc4llb0q5vOCJy8VPKzzsrDGeGAgq27A01BABYOpAKDAACLAAAMIAHFgCDDtZU7udASC+DUAEUgBSbB2H6lFZAjx3SYteEgYWNwzhFFgO5V1YjZ7jJkEgJMwJzUWslCeJeGiiqKhFDfbSPBhR2utVQNgdAHRpDTdJeUsdswtNzVRYUjrbVFsoCWstcUpSVszWo7N0pESaNrYiPN60HQDOLZINtxMTHeEhIuKW6a5RCSrMcntZ8/SWrvIiQtY7S3loUMKHgpAR0NFbWkSdfRp2zqEvO1Ci6wQ7xaau9dVZERrtTaCXNW6W3jt3WCLoTT8KHtHV+ndCB+z6Eyv2Q0084oJXpslKZLMlzsGFlAPEYbwKRpdSQUMetYyrwUpzfCW8BZIa5WhqAshX1OQUB83cKHZCfpPcgc6Jd6OAePd+0DsDz34r/S6/CB6j3boneBiQkHoNjMSgzJCCHl5IZQ2h8NLRMBRouNh6M6V5Lr0I9spZrN33LuCM2I6xnpC4YNku0NFGqPWSbDAAzVnKPrtBLRpc9HG3NqY9Ru9rGKOCaA0xs9PBvBkfsyQs1fpTH0FMJgAAjngVg2h3BCGqDiKgYggiT32JcJpJBA3AJDZRNLORMtUGdKpmNtkYN03grI5MwoACiM8URohJMKH0dj+B4iJOiEEgxyBWGU3iJryBB31pBG8NICBYDmG+PsYbIkxvHGFPaJR/AABC5BJjTqQCNm+HW1u0Si8FdADX4uJawNcB+IIO3Myrf2nNfas3BAHbtxbWlxtIGbRlqKxR1sqJitepkXbrGvYe72pAB3PpLfzei9LpX9gwICtEpgJ3+xxYSywJLHhsAzt3HOztlIqwOfB4hQArcALYQguGO/XBtFCQBTxEk3bAzcoHN7AjPk6Rdaids7mPsfBGJwzlkydvsI7+yQIX7BVv9E29thnnd/3SkNDUSg/YeClPh79ugQGftZf7HofQ6xJBvi2zkCTcapPwcrehQYqGKKa5K1FcrWG9zmfw9p+Z3MSP61BCrpBhnLwXlM7hykFOKIUZG3J/WMAyejDxHb2QtPMtsAV6VMnwwE8UeZ9NmAs35tk/M2K0xWfKPHe0Hzi77hgjnT96rhX12tIUbF79sQ/3vN16QewRPMuNtm+8IXq8DaKMND11QUe3Hy/oHR+drHl2Uux/j7HzPxecThbIRsLYaCqMSAoP1AbCPYzlMuOk+uYgzhdYANS0jgGIMtqSYz5eDVUV9Fq0v77p1QCrJAquSfpnV5NKjKkIHe7Z7HNCHIdSsMQHbDtbODNJ7btF7NUatbNZUFApA6KEEc/GgfgKASQdNW7eA9A8AkHGtEUbRW/MtPAugAgkA0gntegpA0GEIYLfsbArrQ+K9QnSzUnCadddgdg6g6UGjYUc9fsQoO/XHQ5QghdIne9EUR9VNdgCQqg/AtYZ8MQ/gaAyWLgu7ISY+QPB9Pg1NacF9ddTWFNNcbQ2WRXfjaUMQ2Bdg9XceUDFQ+RJcUZS3ODSZG3FeC1e3FNN/PfJIT/Sgb/N3TTNeDmL3YjVzEEP0fwpzJQhIijBQbQjCRIwQtQ2zPDRItwoQ6jMzIfeIxIzQ7QlItuVg9gwCUo1gtw9fVYBrHIEAc4EAdwbwcKL+S4WgM4a0avWMfgTYaLJgR/N0JXapMTQ0MKeZfsRAAZEdfzVwLQ+2G7GmeKGrCZGTXw+TAI9DGqTDaNdTGQSIgjGIkSPTUjSzejGzeiOIxzRjTjbzQAciJk52AJwScwDTMg9BQshrjnMb53MHiQMO9i4uptF2JPgkBAAL8jYyE2AwnUnxCwUCyAAH5+xABL8hhWuDxXfTC0DlUGDno38w4xAyCyRL9lBAaK+yST4DUCCBIA9VKCsCcC7G4AkBOByGS2wCQRhFGLYgAmOGfkVSICLVoGPBYB9CQAN2QliwdmkmLnxGKKQAACZc5TJ9AJSkBr9ZSBRvAGx+TaRdF1sEtxBRSjMNTJTpTLhZSdsZFpIlTLgBQLStSkAdS5T9SIB/xKlkhtAPMBthkkNnSpIbSURUtR8QhMAaA8BqIEx7SS5UMBRbIhT9kzSRRNTgy5Tr8NdisxAYxr90goz81PT2IkB/dKAitR9hSzT0JLgaRMA4AXQEBWlCBQR2kQhKpJTOi2A/R4AUB1VYzmYlT6yXR8zmzDw2zr9To1Tr9HT2yv5JSZzTIuzMAeyB5WJiyAIah/h1t0ByA7QKz0s/RIzozUy4x5S4ztwQQpyGxc4DStydy9zDQDycgqz/SpFzzByS5rzaQug9gxBmh6dnyx9ssfQ/zE05FhQAAfUs1XKC2kcgbc3cu0YswoFgZ0JAII2/QYrAM7LIO5TADXA07MyslM/0/7UC83VmQ0MCh3HM8XOgCi3MmsmUYckIMc1s1QOctgTsyqVcvsj8xUkuVpGgUgGAUssC/4cJOC2QMsiGAAPhgqoCAtfLFNrJUAbLYryA4q4pwh0r4oDOgpBQQofLtHkvgsQsfOUtIrFMLA3LDMPOPJ4DNPIr/PQmopyAT0d2AskEYvMykgLOjJ9Hr2ZgVIZCVOEtEvEo8skpSGktks3AUoCp4CCqnhBEMvvKQuNASvMpMqfK8qPMLNTNsq9POBwPQD9NoBcsoqQ3cp2yAvot8vQiDJlLlNQ1YqbK0rbOXJ4q/n0ojMLJSrgLtM/MvJNEjNS2FIOmIvSxUpoCqu8FquQjrI0o6pbK6o7L0t7IDKwGCCSqmvyscucqIEYqiu8H8scsGuFFKt9K3TFOautNaomoBSSr42jSI1dh1wuVHVoFmM5I5IkGuEnRhCavTJau8H7BhEAECCKUmEQAIIIPztoPrZq0zJSMzvBIZkzlFUz7rXS5SAFtEUB0BXqe4vE3wTTfIKAfq/yCL2jq8gaQbUawaYboaIb4aQrG8vFjSMAxBsbQaHr0bDSEAubTS3ycaQz8aQRbgiau43rpRrrp9KaaBfr2TabAbYFgbWYxbHrpqPK9qIaWa4aEbdx5aKqXs+bcbvBUMdaOjHKk4Y4TbbqzbGb+bQzrb+rozoVJbCaDTBSIVZqiJwkYRxTnaLaYaBKwqS5faxpkataxA7yjTyazSA6Ugg6jJzaQyIbw6IQS5ObE7Rb06HYDSHam0yLjq/zk6YANaaqaKPs6LtdGrNaC7Lb1LGz2L1r5zNq1z3bkr69M72aRqrqfTyrHb5rTqUacxQ62qVq27OLurO7+KkrLqZae4o6iYvrFb+wYrK7laabOTrgGaJ6QyobYQ2aBzEbMbiAk7A7x60bYRobRrdxV6Lh/br7Y6T7PbaRvbl7mlBaybubvqlat6YQd7/rq8D7b7j7Db+7Fxc7uar6U6b6mbj6H6lxYGRbaAK6g636oGwSvbpbxiMrHyel9kAHN7A6QHVaAz9YpJ9aYbT7hqYHjLMqrKsa3ypIfEmHLKvLkamZcHP78G7DvSyrSGXpIM/yyGU6KG96qHYxFraLR8Gq/zzM36p7W7OrZ6Nrly+rF769IH6H3lG9i6jrGLMGx6VGW7NK1qNGO6tGtru7Bq767a3ojHS6THr7FrzH2qZ6dKeruy7GdGeS2a+Gpbiaf7RNukpjlyddFbQM882ADdyAIawoNpukbhmD9Y5Ha6FH66lHwGmbVHLHxzrHuL57dqLrdHoaoGz7H6kbrKaBTHsH770Fo66mGmm736XiY40Geb/S2mQ6j6mnun4HK7EGXbDbOnnGh7Tb5rTGPH2mCnVqimfHSn7GKmnH7apmR6y6chZmwLPHp71HlnbGu6AmaQcGkAI5JaIT5soSn7PqSGN6gGpGAanbD65S9HUSMTwS0AbnSb1hybSGnnqbQGrtGmT7PnMT8Tg55aRGiAxGcgJHt7gXKGzH5mLHFntK57jmF7ymeTKnYauh2itIxgIAgA

https://live.lean-lang.org/#codez=PQWghAUAYg9gTgWwIYBsCWAvJAXNMB2ABAM4DGSAZhTCgCaHVwMAOIzAnAHQQQAqAFgFNCAc0EwEg7HDSlgqMQCM4SWYSFIAbgE9CzJHGzFCACjH5BM0iXSlBIFfgDWhJPnrFsSRWnQZLrvio2sRoxACUrnDC0czRxIL42IK0EEjGggAezLZo2OrazDDYQgnEnIQCwhRoQSiEaFSEJeLRCA3GFACuKCi6cTCaKQxwEs38MAkFRS1l3CDAPEGSxPp2hAAK7Dxd+GhDcFNdhJqEAO6EmTyecF2k2F3RmzTa+BJoqACySMwAysyCawmXiJYjwQgALkqhWEXUiJgA8l18lDeDCTpEzkJohBCIQoJDKqDwYAkwkISOwuMIpBg8FotRwggAIoIRNFhFCAHI4Km0VnsgD6ggAjgKakNCTS6Qzkiy2YJhABeQgAVmu0juDyeG1GihQgnaWMsgipRC5PLx/AFZtVhEAJkSEfBUgDCSEkKiZOCQhLRAMIXSpABk3YpaEhPV4fejNFSQfgwXAACxRv1nKkUlPCK542qeABalhgGahBdG5ORVIA4olLGooa73eGvYQyTqYMwqb8uswioZnQR6bgCITgwhQ03I63Rh28b9BPoVHqOYRR+OI96p+2qTBFAk4ENaHGE4SG5YJxuVyGw+uW0T4/BE1Sin1vsxCRsXm8EB8UK//oC7wTZMKSpAAlNwnAAIRgXZaAAQV6ABVfBqDoWoRGMVFiSTW82xnQhHCgmD3AFRoKAFKABX8MsISpPFAAAiSofWwxMABpCHA5xoNghCUGQ1D6XwDCmMAFMI9BeV9OAJXhCGVAAGKkEgXbx9VIhAcjQQRiAFQjuPcSE6MIRi4JPN0z3XdjGJQN0Ryvc9WMM2d5wMFThGs9oyU4oieKQlCaEE4STB3PcDyPcETPc8IqV04jaDUjStIFJSXKXAVzFraxaLxBjCBM+szI9L1LMIdzbLHa8iscwhqwsKxctvLse3gbB+3cPI8CIUqSSqry9Pg3yBPQ4wgt3SxQuw+rIoa5zF31Eq3R4HBpDQRRkWEABtXMvHwOwAF1Nl1fUEE4LbSyLCsIGWLS1mENslwQHhNAMD4l1MDZ30Og0oogFp4ANalaTgQTGQFPl5UEAUaXjbaUU2Thn20SSpSBmVmX5BVZNtCFFSpDZ4Ykn5ODBwURTFfYTQgUAQAgAADKAacIPkAXcYwCD6QhhxaVxiASMd9XoZJ7zgdi3nyYcJguEocGaCaznSPRRloO4UnmRZfrafEdOuwEjAFQWE1IvkkjybRDIAbzgwBAglywAggnfThT0KrwAF9CDN9zrfcu2oTx1cKpdwyTH4GSfc4YKxpSMKmCt+aEGt5U8fD/dI4muC7a9yIsuyvGEckgkTET0bk8PVPPbdS3IgT/GX0J/PC5ClOhdt2Obcz5VFFNvFQnUwh1uD3aeCpiBGFEGs6vIRtGebNwPG7XtsBAGl1JwFa5ppwBu4Bphy6ZMJlK8IOSGbIwgN6P4wEB6XANPIXAhnZ5LZsEVWfqEP72ko6iYFIqgkpm1zA7ynDR2554SlVDn7EBgd+CALxjVDKuV4T8F+PbRq89WqDg6rHTOhkc4E2YFJN6Yci7jSbhFN0+85KEDEnjOcylXpgPbp3AG0Nbj3HgFSAA7Q0JIZZ+BQEMvwLQwh+BeXtr1WKvF+L+SGoQpOJDjxkIQG3KqBdOAxVgt/ciH9CyEAFOETgAAmdQ/DsqECyEge4cN1EkTQOpdAiUH6uTSmPNQij1AmSQeoLynDuHSBgOoWhAihFeIgmIiCfVJF+TQkJYa9cI4l1IVgyEONTF4jxo41KtiEraWsfQNxSD5yGXMZY1RuTNEUSojovRnAACMITnA8HVv9LIYRdYIy/D+AUyBmACjOHkK0Xg4BiGwAKAYAJDCaUwoZQAwET4lWABH2n53hfB+P+aweMo7JjxhSByqS5kAlIJwZGwNZToyVLaQA5ERVWMvbYBFkjKx3thAiyVU0mcDgXVEyrZOCoOaug9qw4uqvOyiYKA8zDl1yIQ3BJCiknySoXDWhKU5pTWxoQDu0VBA1AsIQQAF+S4JrswdiBLEaE2JgqIUopxSCHYgAfgFIAS/IqS1D8ZNGy0CAlUmKfkPG2jRjlIyXNfJHjfiNNfhrNwxAziWD1l/AY91SLaW0FpAypjZlgoOe+JZ34Vl/E1RslicMdkqI1YCI5gMTlo3BpjFUkQrl7JMDc0OdyioPLAXDZ5lU9lvI+a43CPy55/IHACzqNlurepBaaiFsjiGN1hVNeF1Cfl/3oeQ5ReIWmeG0u05ZKAuk/F6f0vWBhhmjOnJYXAKqC7JM2N9RI9A7pHR4PWzY2wgA

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOD0AtAIQ4AqqwAznAGbDoCmcIEAJo+lQFw4BUcGFCQA7KrUZQ4VAJ5UYjEDQgjpAVywBzKBDVg46FDGABjRlQA0/FsBGgk6QmwggktuLcYBHNQ+DHzKwEqDW1dMCdGMEYRDhF4KhM/EU04NhQkOAADNiyguCQseWETeE1GF0YhU0J6AA9GNkJIW3goRhMITTtjFQA6HEJ8PBEkEHMwJDM4AAUAVjw1OwA3SSpmNThlvHXS4BU4MmExCSgAYWhGPGWkKGBCpjgAbwBxOG5DmWi4NQBfOAA2i8dHo4C8ALo7IRqUpqdqHY7iSQAZTkChAcAAFG8PmQvhsAJSA4HhMHguAAd1QkiucDgACVOO84MjQiD9G9AEmELLZpK5sx0YBwdPa6AA+u1aOhmYAAIjgAAkLAymfKFcK4KKxUJRDQPnKngBBOAAITgZ1+SsZ0qNpu5VpNZrgdqZRrO6s1MAgYseeueAGkFRbldKA6ruQHACZEapFnDFtloEvM1VKsv9CrgABkg/bQ07M3Ao2Hg1iA4BkokzRIzUKgMJgcOYCFs9nQABEXG4RC2Muq6djmXjvmoiUD2WSsWRkf3EadUfJFGCiVSaeqMR9WVpR/z12FQS8V4npb7FYdkX17ZiMfKifL9yB3L6nqGgxOz0zc9zLwW4H7rrd7lhHkxCcpx1Gc0XnF4CRwG47geZhMQQFtmUbOxXFbdtbC7GBMjeCcoJwNAKnaDE71Qhw21cWxvUYOMRATCAE0eJ5VQDNdeV3f5MVQeVWPTKM/SJXg6TpRC+k/Qs4HLUSMVYgBeOAsBkdVUCQVY4FQK0QF4l9z2k78iTkxAWzEg9v2U1TmA0pMpFxU9dOMmTJIVa93nkl9NXjRNilMeArPQLT1J48y1NQVcjLEvjwsc8tVW4eTpLFUj1MZYp1SoUBJkBTzOhAEByTUdKUnUkA8BiNgEVAyQLnaHYOl6VRkSSTAUgNWIADk1F/WCAOYV5+3xH5/hHPlIWgv84PHSdcWnFFwIxSCxu6wDEOQps0IojssJwk98OKWt6xZJrbE0LaeyxHFPkHYcSV3SFhMmkCTlmud5qJBCkI+FDmw2zCMjBHbKWpGq6XKtiNz5PM2pQdV6kaFtQGZbdNzzJGIe5KGYBh4AGjYeGQEStRxTYMVyneM79RYxH2I5INVX4vNYdxhHcwEcrVUAUyI0jMnAOFoOARE2TFkQ+w7khOv7cMnRC3tUD4Mbe2KeXB3dBLgDHXPVYA+bFRHjLZuB5IABkEalVGNzh1ixVQAGoWT19NCDgABGIl8Dtvo2bwQjLgxRm8YJomSdpYShZFxqxa2/7gOl55KbBncaaxbjeLp/Syfu4W+j95n0wETP9c5/Pvw1ulM+z/GQEJsVidJ5PStiUXms0Vq2A62q9gOZFMDMFsqjq/YRC6/8mIugcNiGm6OVGmDh/g4DpsqqBZ3RBdFtnrEVs+tbyIwzsJZ2teJtDxGjpSSPJaM3boVheEu9MRgADFhHGCloAAazOvtcQGodiU3O6Q7zwqk9Jec0FwbxFl9dau9z4H3usfNcp9xbYSjlLFsb0AAa/VvjLEXEDYOZAkBqBeAAUWZOrbkWDuQzEFOqF4FQH7Y0aBcEQsslYJ3+ujFAeYqECggEKGMnRuj+AHunYScpVB1CVIQ4hZDJFwEACmEcA5SK1RruJU9CICMJxiw1QqpMQCwenFAG71XKXztvzZycA6he2pD7OAEA75mDFJ0Vh/dlj+BkHGWgCZyiVGTGKRmYoWjxCoGdJ4WDv44M4siB+iNu6P2fowV+UA36oKMhYjBUF4FsPlliOozIsliNLg/PoMjSGWIKQos6dIVFU2VhyJUsS+iaO0cwlQeiraC3nm5ZEb1N7xXQRYvRRIClxXVM09oQieiiMkdWfa8IABqohqCUBSAgdgnBP6jx/tdf+n8gFHEXsvCC/TIHb3QpRPeKDJbZJDsLE+Ed97RyGZiSJl1mC4MBsuOkyy7BUGpFQY0nAIAUnqRw/kFC4C8Jofw9UfjXEiG8QmG4/zAXFOUViWJ8T75PzGMk9+6SVoPKKZiVR1NwGYjSXLFAb0xnQoJFYe6JSWkMKYWwXR6Y0lVLgH81Z5hgXoFBVy6x8yb7MF0e4xgGyODoG2dgwkf8Rqf3eWPLYeCflmg6VKwpeZYVCgInY4icBEVSrFI4hJLiVIlAUHcAAXigAe4TVUDWWL8T+2K1wJLxS/QlF9iVISyZ/M4CBmSSr2KsGVTI3hBvgfS0luTaWfzFKgTlHwQ19HDcYNSdRBJnWaeUuR1jFE1MxeShpYImmlNaeyzl+jDFASmr0s5ZiY4PJGcW4xil1SMDqFMeAkyOhdBmQcOZhqiLzgtffFx2qI2eORWKVFqzjrOoVVsd18DPUsm9UklJaT/VIRJXc3sizQ0fD5QC46UbpQHsyceq25DaX5MKXmjOpTC2VJLcyst4LNxKlPX0C9gLBXCvrd0ptJiBnmPbVYsZ8lu10lcXtUo0B1QAHaPDxB0OpGR0ZhK9v7ViADCKOkLqXQC8wLI4mqh1rmvoTssRC1KVM4dIjR3WIJPRnDRDnLocw0ICA6kgNnUlJ4LFzGh3CPqpUzjAAmOAAB+MUZ1WjYZvPdAjKZMTEYqIisjKyKM0GxTRjjfR5NcSA7xnAZVt3317goDug9rMN3mDgIAA

https://live.lean-lang.org/#codez=PQWghAUAVABASgUwA4CcEGcEDsAuBDHASwHssQcALBYtIgYxkKyQFcd0YAKACWIHcEMAG4I6OGhwDUMdCyRIaOGABsEAWzV4AlDDxpdAI3Q4UeMQgAmujhQCeCyhgwA6aDAAqVGADMmeZTAsWIQiKOj+wFikQnjB6BRMAOYg3jQg/sogAAboWTCONOqMHKjEIlbeKMRq+VSYMHYOdS4QIMAQEFh4ahhIZoIACgBMHUEhCGGCLMIwfDAAHh10ynjoHHAAygDCpDgI80p8VGgQMDADhO72ggBcHteBpzBIlw93V0iCQk8A6gBiQRgdwuH0EgCTCe6fWZPABqAKwQOeryhENBCyeG0RaJYsP8WIe3zOTGMAC0JsQYXi7mSqjBKcongBJXAIRKmAJ3ADeaCQACFCIlESDrgBfGAQ/6Ann8wUQ7nIDaaZQcpGgsUQuFShVKgIQzEa/xPHZYUKJDCI+V8gVC5EIdUwSUI6XWuU8xUZREvNXiunwmBunU+/XnKpIJ68AQAGUIAGtbjBLTKbd6JX7nbKQ8Qw2cAHI0JWEABelgt6eTop9jv9yCTEIGoaN1T6Yg2cgUKBwAFliBYc6Wa9bgbb7VWy3WG2cACIIHAAQSMAHksAgl635Ip+1bBUOUw60wOM/Ws0887gUCFCP4NglvEouWWdxXU1qtz6j2GIAQTIQDGxBABtYl8CwOgEAAXXgbZdn2HBnCAmkKUNCBMDEEgsA6GJzzwAxVBgf9NmNPYDjAjC9EvHDBE4C4AAZEQI6CDmcYVPh0Th0Fou56JZRiNi0DpjBQFgxBYfQAFEDgmLplAjBBmVYdhZmOBAnn2QhjHQAB9Ch+AQDSRDEGggSeM5AGAiB06Kg7jYKrGiABpjLOSDCJg5wZOjONzMAciInIY2C8xQAtiysH4njoJszBwDTZHXDsNOIbwtJ0ozHJgQAAIgTH4LOcxibMIaiRVsnyrNcnT3METKwQcs4uKI2CdjUZscDXdsux7PsQrOCwZw07DNNIXTSCittFDihLtIEZLHPSzlMs4yzaucXL8sKmqXLc2NyvFKqioW6c50XZdV2GjsHSeKIzwvfwopvSL4sSiabgc6bZp2lyloK17GPWjyKu21bGNPb8hEvZRr0IW9TuQkwhJwETBHEvYUCk5k9jZfw5LYDgjgmZSzjCk0JjNTSMii0aNLChqIqGmK7yejKst8xa/Roj7/rq8KW2O1re3MyqUrOaaAw9Obstgr0K04GEGeKzUnW1DJWI4EXGd4+z+cctnnGNU1zUyqX0CeJhUfZDSmC6z4sC63Ayb6hKusi3q4uXSaBfp5Xivelb5pcvb53QJcVywZqN1+9XBfl5VpYW8XPjFSWo5c2XqyQd1lUVhOeK0NX1c+2CUdZdlzP1mAAF5c+cfO0YCPWZGos7oliNSEiwRINIMWwNPPRIKEikxYnQFY9hdtK3fLz2/u9xj6sa4OO27HmKvLwHz2Bq8bt57b0qFyP3ej21CrMqXd8T/cU51bP1c1yvC5r9iYEAAyIYDrqHBOEsSJKR9HmExxScaecb4wI0kv4GSGMFI0UNiyKuiIgGf2UNfL+8kOA0Vrh0AoaAaiqXUhpH4GkxihHCMoDSexjD6XECgBynAKAIxgR/ZG39wF5VrjoR6KUzIvU1ktC+U1k6pxVJrGOCAD50gzrBJO29lDcJSpwdKSty4bC9qLLW0RCa6xEegHQnltpnBkTIURzgFHlwQdXdRpcjFQJvuo6imjtFcFkfowxV8LF4lvg/J+LCy7tyeCgOgqxzTUMYgA5wWD2D3V0mQwyfBCCUBgIAC/IfiFQoDJQqWl/JqEAJfk/88AiAaNPCK+i8mcxpvPdqQIS4OQCbBIJFNGrUxamTABDQZJZJyRQPa+jfYHUDrPJQs1ykpUqc4IJ9sepGCdgNLAdSRp3UaUknSLTBAUGXiEfRyzV6g3Xn0ipCMhk6WcOdIGINrrg1umNJKcyBDeIQL4Z28TCoAH4NKZKJGeYgvCdTeN8ZgGwOyjYF38PshucRm6t3bp3AUPdiGmCwAPAgizClKCWbsFe7yPRRJibEmEiSDB+OedWG5ghMUPI0sS4leKADtjBXkyAcvsfJgy/lV2cPjHWxNlSkzujUqm0UWq5I5kofWTxKVG1pAbFKdKxANF+c45QcEZWm0tsgbAVtTkcrtt1R2/UGjtMFWcYV1KbDsQqdkxZcinHGxcaYsu5r/kmP1hxfp/MGUyrlRaohZslWKutndW2GkRmaudm0mc6jjU5OPoxYxRda5mIdTALx6tfHKDoLYm10Db60WtZPPOMqo1K08bYGQhBKaBHQEkBo6BnDoFsBoWxGkY1lPLXXcV8x6U4vqJQNSHRQAgAgNrbAhBsBKDClUZUegC2aBwHQEFtRBBdBQKYIgOTjBwp6LgR6qQUAzpkN0QQU7iCYARFkH4eRYhWAQGYCgMAsiAAHgLIhVHBUrdcUQw6BiDKD/MoAtLLVG4F0JbGA51iy0g3boSOOQsiuDaBAdBRQQmaVwRunq7KXgaUA+SJDRCxWOSoTQu4sD6FIPOEw9iLCHLsP0VwzeqKd7l0EcIo+5dxER0kbY3RZqs0GMUYzPtKAia5pgN5VNlji6P2sQ2+N/ovnmjgzgvBwQCFXRITgCJm6qJMJuGXGiitY0kalQcWY0TL13IaD8PFaACVxISTAR5eKRVvIkZ8vxNhMoSIMxirFDQWUpIoPjYwiS0NVDM9cpghKPM2cgSYN5WGJVKFiT56IMh/OkCA1FzJEBlUdGVecEYQA

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0CCmSAzgK5T4Aqq+0AnjgOJQQlh6GlRJbr4CiARxLAAbgChQkWIhQZs7YmUrU6CzvjxIwE8NHjI0mXAUXkqNKPRPq8JGCSTp0tAMrAAdgHMS6JFB1S+rJGakrmqtZKOBS0YPgAxr5ERPhEOAAKzFjcwJgwtGJiEHHucETxxfgAJogcYSqWRSW1psoWBWLuSCCpYEjx+HDpAIyFKfEwwBClAMLQ+IUifsDcvHAA3oCNwHAAXHAxcQBUAL5wANqRXDz4Ln0DcJsAuoUA9AC0b2IAkgBmcAAGgB7gOAAQTgAF44MN/nAkO4akC4AAKP6AbwIAJ0AclBAEoIXAAAz/AA0cDQ+FKQJhwCIcBAdgcTloZQ83l8UDgAHdgGgAYCcCAtHAfv8cGI3i8xOT5iA6QzHM43F4fH4APqCsCqiA/VU/HzoVVgcigJCefCq9z6sRwG3I4F7S6DTZ4s5fIiZCDZLC5Hm0R1wQHPW0bP57baAJMIHqckahQy1OKtBj8cdbbeswXsXPh4Jto6gM/GyIms/AQSngzHAQXgWDIcNy7aY0bBntgSi4BjsWX8QS8TtUzbgYAh8kAGQQBgVC0OQrAFG3kH4eQaAC/IQYAc3FJ+ZwFXA6FJAH5VfvVYBL8lTAHa4KgkCJBrGPDyWwHQXBAAZEyMAJUS7OB8AByP4ASoQ6B9tOs7Biy4DnKgVZBraV43pegIkO4ohfsCJY4MhqGQkiwxfr+AFASBcAzgOtpEJIZHxI48RkYOoKrvi6HZphKEiHAbxPhmoF0eRkhIHAJAUV4yI9K0qrbmA6B2rskKAni+aXguKEwPgDbBqq+K4fhf6AY4eKcXhOygRBYBQUhbEbjBvGaZCBKySRzIUeA56Xtet4agWSL8hqwp4rWhIOaR4GmQJFx1OQE6aloUnMrGl4go8gnCZ4l7NmRzl9OckkGjlSVCayl6eYU0rkLK7gQDAqr9OqWhajqepOIaxqCmaFpWhW9qFuQDwum6Hpej6+T+oGZHrHGEZRsi8UOhFiZ+WNBYllNMYFpcxbZriZGVtWz51up03NmhyJoliuI9n2ZEADUyYAVkTjr5yZBWBHgwMwCUzKm8EeVoXk+ZO/k9s9GX8ecjpRdVYCxUpCX5SlaXkF97mISC9mtntgXGR9RW/UjCF7NpewEXpwFA1jwW2tR6C0SFhPfrpRFMc+5NOZI5mJTZZOQtBqOpvgAAe/TwNM5ruOaABe+DvWgNKFBSNRzIjYjjJM0z7Fw7hEL4qvuIsyzzesDBfgc+AnOcIJVFUTAsGZDBJeFpjFncgx22Dc3XBbNR24UVT4H8b1wlrKCDEigATwF+DB9nARuRkbWN6qUJAQgAfIJcAANRwKHJUNPgspiQm1yqgHmvayH4d7JHX7rdcyIl0HqnIhXkKhzixEU5lYX12XcOFUiNe8IIwgiDgSCW/+wCeKg8CtwK7u8MXEAAGLIXrUArLX3nVxFLt9e6WQ5Hkfo7wGzxiO8nwglgRABxMcDkFJ/R5xS8A/NAZLULCXTOJM8RwAAEkgYA5AOQeDAHYMUEoxC+z+C4VAwAfgwCzH0LgkwRJ7A9GZYyqZAAARFnCOpJw5vnsuGMigBgImZnAZaDBSQDxuJtMEgByIi4viPCzC2xIm7sHJuDlW54k7OdOyOcLB5zlPYBUrhWQqigMXDWDdzTalVEQeBiDkF+BQKybaqAUhYKoSopB+AUEaJElvLG8k8TrArtHPMViiGEkusGYcY5/pmU4XIsuPCsZ8OBnOaiKRaTaMMfg1A4duS8hXBuEEVkokI3wKeG0AshZkXpOIpkSo2Rqg1PVXU+pmr4BNG1S0TgZJmIOjadsWMuGNzDrwtuvEYxTjpPPc0VTy61LKQlFGsThEyjgBVKq+AhCiEcC/WRgcy7ZOUQggxRi0GeC0Tor8cDplqNQX3e0ck24bCsQwGxX47G9l2NdO6D0hRuPGdwmpXitnsKinXdxlzm5Zy2fdeSPi4CvXeqgVMUA/GpEvIs8OISuQ8lQHACJCVokbmbPEuAiSJjbX6dVeItVNSKMagaZsBTRb6hKZs+pjTWmeJbnU2mM1IQFyLEXIlVySUdMUjzWJCkcCjDEPLdWFydZy3hEMUYQA


c. Problem and proof in Lean using agent team and prover agent:
Ask GPT-5.2 Pro Extended thinking or Claude Code to think what team would best prove and explore the problem from diverse angles including the formal prover.
Ask Claude Code create the team, and use the team and formal prover agent to formalize the problem in Lean (problem.lean)
Ask Claude Code to check that the problem in Lean compiles, and back translate the compiled problem in Lean into natural language (problem.lean-nl.txt)
Ask GPT-5.2 Pro Extended thinking to check if the original problem (problem.txt) in natural language is mathematically equivalent to the back-translated problem (problem.lean-nl.txt).
If they are not equivalent, then ask the team and agent to fix the Lean formalization
and repeat, until the problem formulation both compiles, and its back translation is mathematically equivalent to the original problem.
Ask Claude Code to use a team including the lean agent to formally solve the problem (proof.lean), given:
the problem in natural language (problem.txt), problem in Lean (problem.lean), natural language solution (proof.txt)
Ask Claude Code to use a team including the lean agent to check that the Lean proof compiles, without sorry statements or axioms.


Submission:
Submit the following files on the Google Drive under Homeworks/2/Your Directory:
problem.txt, problem.lean, problem.lean-nl.txt, proof.txt, proof.lean, proof.lean-nl.txt


Out: 2/9/2026 Due: 2/23/2026