Machine Heart report
Edits: Egg sauce, boat
After trying GPT-4, Tao Zhexuan used Github Copilot.
This time, his trial scenario is to learn the Lean language and use its formal mathematical theorems.
For large models, formal theorem proofs are also a challenge. A formal proof is essentially a computer program, but unlike traditional programs in C++ or Python, the correctness of the proof can be verified with a proof assistant (such as the Lean language). Theorem proofs are a special form of code generation that is very rigorous in evaluation and leaves no room for illusions in the model.
And the theorem mentioned by Tao Zhexuan comes from a paper on October 9:
This proof in the paper is less than one page, but Tao's formal proof uses 200 lines of Lean language.
For example, in the paper, Tao Zhexuan only asserts that for any case of a>0,
It's convex on real numbers because it's a regular calculus exercise, and then Jensen's inequality is called, but it takes about 50 lines of code to write all the details.
Tao said Github copilot's ability to correctly predict multiple lines of code for various routine verifications and infer the direction he wanted from clues such as the name of the theorem was "incredible."
Lean's "rewrite" strategy is indispensable because it modifies lengthy assumptions or goals through targeted substitutions without having to type the expression in its entirety.
"When writing proofs in LaTeX, I often roughly mimic this approach, cutting and pasting the lengthy expressions I'm dealing with from one line to the next and then making targeted edits, but this sometimes results in typos spreading across multiple lines in the document, so it's good to be able to rewrite them in an automated and verifiable way."
The paper also mentions an inequality that satisfies any k, l, n
rule
Tao Zhexuan said that the next goal is to establish a simple version of this inequality, the inequality in the paper (1.8):
This part of the proof mainly uses the knowledge of calculus, but there is a difficulty in the use of asymptotic notation. Tao Zhexuan said that although the follow-up argument will be time-consuming, it is not particularly difficult.
However, current tools still have some limitations, for example, rewriting expressions that involve binding variables, such as summation variables in a series, is not always easy to complete. He looks forward to the day when people can simply ask for natural language LLM for such conversions...
Reference link: https://mathstodon.xyz/@tao/111271244206606941