LeanAgent Proofs

[Adarsh321123]

LeanAgent discovers proofs for theorems with the sorry keyword.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[mo271]

Thanks for the pull request!
Only the change in FormalBook/Chapter_08.lean is useful.

• Proving wedderburn with Field.toIsField is not at all what the intention of the project is: we want to follow the proof provided in Proofs from the book. Of course Field.toIsField also uses a proof of wedderburn (which happens to follow somewhat closely the proof from the book, but we want to recreate it here, not just invoke it.)
• Similarly "exact book.quadratic_reciprocity.quadratic_reciprocity_1 p q hp hq" is not useful, since we are planning to give a different proof here.

[mo271]

You write in the paper you reference above:
"In the Formal Book repository, LeanAgent progresses from proving basic real analysis
and number theory theorems to mastering advanced abstract algebra, exemplified by its proof of Wedderburn’s
Little Theorem"
I think you are really misunderstanding what is going on: It didn't master advanced abstract algebra, but rather there seems to be a misunderstanding of what the point of this repository is. The proof it "found" here in number theory are also trivial, there are two theorems quadratic_reciprocity_1 and quadratic_reciprocity_2 with the same statement where I the plan was to give two different proofs, of course quadratic_reciprocity_2 can be proved using quadratic_reciprocity_1.
The result in basic real analysis is a call to linarith, which works.