Zulip Chat Archive
Stream: mathlib4
Topic: !4#4777 NumberTheory.Bertrand
Antoine Chambert-Loir (Jun 25 2023 at 15:41):
It seems that the proof of the Bertrand Postulate on !4#4777 now compiles.
However the way I could prove the two inequalities 0 ≤ f 18 and f 512 ≤ 0 is probably more complicated than necessary.
Last updated: May 02 2025 at 03:31 UTC