戻る

The tools are still steadily improving though. In the near future one can envisage an AI layer on top of Lean in which individual steps in a proof (e.g., "rearrange the previous expression into an upper bound for $|s_n{|}^{1/n}$") could be described in Mathematical English to the AI, who could then attempt to execute it in Lean, perhaps with the assistance of a computer algebra package.

There is a noticeable difference in the power level of Lean's tools with regards to using equalities, and with regards to using inequalities. For instance, using the inequality
$$|s_n{|}^{-1/n}\le \underset{k^{\prime }=k,k+1}{max}$$ $$(2n{)}^{\frac{1}{2}\log \frac{n-1}{n-k^{\prime }-1}}(|s_{k^{\prime }}|/|s_n|{)}^{1/(n-k^{\prime })}$$
mentioned above, I can easily tell Lean to "use the fact that $\log \frac{x}{y}=\log x-\log y$ when $x,y>0$" in a single command `rw [<-Real.log_div] at h` (where `h` is the name assigned to the inequality), and it will automatically locate where in the inequality this law can be applied, and apply it (adding the positivity hypotheses as additional goals to be proven later, but Lean also has a very good tool `positivity` for doing this). But if instead I want to apply the inequality $\log x\le x-1$ (which is also provided by Lean as `Real.log_le_sub_one_of_pos`), this is substantially more tedious, and I have to write out several intermediate steps to tell Lean how to use this inequality. But I view this more as a limitation of the current state of the art of Lean tools (which may well change in coming months or years), and not as a fundamental limitation of the formal proof verification paradigm.

@tao Thankfully this constant is smaller than the "constants allowed in real math" mandated by xkcd https://xkcd.com/899/ haha

@agnishom @tao A possible approach is the following:
8/3 = 1 + 1 + 1/2 + 1/6 < e < 1 + 1 + 1/2 + 1/6 + 1/18 + ... = 11/4, so exp(4/e) < (11/4)^(3/2) = sqrt((11/4)^3) = sqrt(1331/64). And then sqrt(1331/32) < 7 because 1331 < 1568 = 32 * 7 * 7.