5 ms·

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialist

• ted_dunning 2y ago
  I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e. It would be annoying to have to code that kind of statement every time, but it wouldn't add that much to the effort. Formalizing is still enormously hard, but I don't think that this is the example to hang the argument on.
• vouaobrasil 2y ago
  > but to truly provide all the details would make papers far, far longer. I think what we need in math is that eventually, a collection of frequently cited and closely related papers should be rewritten into a much longer book format. Of course some people do that, but they hardly get much credit for it. It should be much more incentivated, and a core part of grant proposals.
  • jll29 2y ago
    Donald Knuth's literate computing could be an example to follow: combine lean prove language with inline English human language that explains it. Then, Lean files can be fed into Lean to check the proof, and LaTeX files can be fed into LaTeX to produce the book that explains it all to us mere mortals.
    • ykonstant 2y ago
      This is already happening, by the way, and some Lean projects are being written in this way. Not only for the reader, but the proof writers themselves tend to need this to navigate their own code. Also check Lean 4 Blueprint, which is a component in this direction.
    • robinzfc 2y ago
      Isabelle proving environment implements this idea since at least 2005 when I started using it. One can interleave formal proofs and informal commentary in a theory file and one of the artifacts is a "proof document" that is a result of LaTeX processing of the file. Other options exist as well where the file is exported to HTML with hyperlinks to theorems and definitions referenced in a proof. There are also custom HTML renderers (since 2008) where a reader can expand parts of the structured proof when they want to see more details.
      • zozbot234 2y ago
        Agda 1 (more specifically, the included UI program known as Alfa) implemented an automated translation from formal proof to natural language, driven via Grammatical Framework. This requires writing snippets of code to translate every single part of the formal language to its natural language equivalents, at varying levels of verboseness - for example, (add a b) could become "a + b", "the addition of a and b", "adding b to a" and so on. Similar for proof steps such as "We proceed by induction on n", properties such as "is commutative" etc. The idea gets reimplemented every now and then, in a variety of systems. Of course the most compelling feature is being able to "expand out" proof steps to any desired level of detail.
• ykonstant 2y ago
  The example you gave, however, is obvious to every graduate student in any field that touches analysis or asymptotics. That is not the real problem; the real problem is proof by assertion of proof: "Lemma 4.12 is derived by standard techniques as in [3]; so with that lemma in hand, the theorem follows by applying the arguments of Doctorberg [5] to the standard tower of Ermegerds." Too many papers follow this pattern, especially for the more tedious parts. The two problems are that it makes the lives of students and postdocs torture, and that the experts tend to agree without sufficient scrutiny of the details (and the two problems are intrinsically connected: the surviving students are "trained" to accept those kinds of leaps and proliferate the practice). Frustratingly, I am often being told that this pattern is necessary because otherwise papers will be enormous---like I am some kind of blithering idiot who doesn't know how easily papers can explode in length. Of course we cannot let papers explode in length, but there are ways to tame the length of papers without resorting to nonsense like the above. For example, the above snippet, abstracted from an actual paper, can be converted to a proof verifiable by postdocs in two short paragraphs with some effort (that I went through). The real motive behind those objections is that authors would need to take significantly more time to write a proper paper, and even worse, we would need actual editors (gasp!) from journals to perform non-trivial work.
  • impendia 2y ago
    I strongly agree with you, in the sense that many papers provide far fewer details than they should, and reading them is considered something of a hazing ritual for students and postdocs. (I understand that this is more common in specialties other than my own.) The blog post seems to be asserting a rather extreme point of view, in that even the example I gave is (arguably!) unacceptable to present without any proof. That's what I'm providing a counterpoint to.
    • ykonstant 2y ago
      > (I understand that this is more common in specialties other than my own.) True, analytic number theory does have a much better standard of proof, if we disregard some legacy left from Bourgain's early work.
  • 2y ago
• zozbot234 2y ago
  > there exist constants C, X > 0 such that for every real number x > X, we have >> log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx. These problems are only "uninteresting" to the extent that they can be "proven" by automated computation. So the interesting part of the problem is to write some completely formalized equivalent to a CAS (computer algebra system - think Mathematica or Maple, although these are not at all free from errors or bugs!) that might be able to dispatch these questions easily. Formalization systems can already simplify expressions in rings or fields (i.e. do routine school-level algebra), and answering some of these questions about limits or asymptotics is roughly comparable.
  • impendia 2y ago
    The problems are uninteresting in the sense that the audience for these papers doesn't find them interesting. In particular, I'm not making any sort of logical claim -- rather, I know many of the people who read and write these papers, and I have a pretty good idea of their taste in mathematical writing.
    • zozbot234 2y ago
      Well, you did claim that the problem could be worked out with simply high school math. It would certainly be 'interesting' if such problems could not be answered by automated means. (For example, I think many mathematicians would find the IMO problems interesting, even though the statements are specifically chosen to be understandable to high-school students.) The problem of how to write an automated procedure that might answer problems similar to the one you stated, and what kinds of "hints" might then be needed to make the procedure work for any given instance of the problem, is also interesting for similar reasons.
• brap 2y ago
  >Here is an elementary example, which could be worked out by anyone with a good background in high school math WTF >i.e. the left-side is big-O of the right. Oh.
  • dogboat 2y ago
    I didn't learn big O at high school though.
  • wbl 2y ago
    Calc AB covers it, and BC certainly gives you enough for a proof.
  • NooneAtAll3 2y ago
    "the proof is trivial" "but can you prove it? [10 minutes of intense staring and thinking] "yes, it is trivial"
• rstuart4133 2y ago
  > I don't think this is easily resolved. It is technically resolvable. Just insist on Lean (or some other formal verifier) proofs for everything. It looks to me like math is heading that way, but a lot of mathematicians will have to die before its the accepted practice. Mathematicians who are already doing formal proofs are discovering it have the same properties as shared computer code. Those properties have have lead to most of the code executed on the planet being open source source, despite the fact you can't make money directly from it. Code is easy to share, easy to collaborate on, and in the case of formal proofs easy to trust. It is tedious to write, but collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff. Code isn't self documenting unless it's very well written, but even horrible code is far better at documenting what it does than what you are describing.
  • zozbot234 2y ago
    > Just insist on Lean (or some other formal verifier) proofs for everything. This is not an easy change at all. Some subfields of math rely on a huge amount of prereqs, that all have to be formalized before current research in that field can insist on formal proofs for everything as a matter of course. This is the problem that the Lean mathlib folks are trying to address, and it's a whole lot of work. The OP discusses a fraction of that work - namely, formalizing every prereq for modern proofs of FLT - that is expected to take several years on its own.
  • eab- 2y ago
    > Just insist on Lean (or some other formal verifier) proofs for everything Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)
    • ykonstant 2y ago
      I agree, although I don't see a better solution: typeclass inference is trying to "quasi-solve" higher unification, which is unsolvable. The core tactics writers are already doing wizard-level stuff and there is more to come, but the challenge is immense. By the way, if you are a meta-programming wizard and/or a Prolog wizard, please consider learning Lean 4 or another tactics based proof assistant. I think they will all welcome expert assistance in the development of better tactics and the improvement and debugging of current ones.
• devit 2y ago
  I don't think that's a good example, since it's obviously provably true and the proof is also obvious (either use well-known lemmas like log(poly(x)) in O(x^a) or show that lim_x->inf lhs/x = 0 via L'Hôpital's rule, differentiation algorithms and well-known limits at infinity).
• bandrami 2y ago
  Is there really not a centralized corpus of that kind of fundamental result you guys can use? I would have assumed that was "theorem #44756" in a giant tome you all had in your bookshelf somewhere.
  • nicf 2y ago
    Nope. Many important results have names that are familiar to everyone in the subfield, so you might say "by So-and-So's Lemma, this module is finitely generated". Failing that, you could maybe cite a paper or a book where the result appears, like "We can then conclude using Corollary 14.7 from [31] that...", where [31] is in your bibliography.
• rocqua 2y ago
  I think the resolution is being much less strict on paper appendix size. And slightly shortening the main body of a paper. Let the main text communicate to the experts. Let the appendix fill things in for those looking to learn, and for the experts who are sceptical.
• saberience 2y ago
  log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx. I don't get why this is true. If C is 1 and x is 2 log(x^2+1) sqrt(2) + x/exp(sqrt(4*2 + 3)) is not less than 2.
  • jsvlrtmred 2y ago
    The statement wasn't that it's true in general - only that there existing constants C and X>0 for which it is true for all x>X.
• imprime 2y ago
  To prove that you divide both sides by x and take the limit for x -> inf, applying L'Hopital rule the limit is zero, so there is such a C, any number greater than zero. The existence of such X is just the definition of limit when x tends to inf. Another way, just using a cas (like maxima) to compute such limit: (%i1) limit( (log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4*x + 3)))/x,x,inf); the result is zero.
• wbl 2y ago
  I think if you let C=3 it isn't that long. The first two terms are less than x for x>5, the last term is also less than x for all positive x, done. Those lemmas are pretty easy to figure out.
  • LegionMammal978 2y ago
    It's not that trivial if we really insist on all the details. Let's assume x > 0 throughout. We can take sqrt(x) < x as a freebie. An important lemma we need is that if f(x) is continuous on [a,b] and f'(x) > 0 on (a,b), then f(a) < f(b). For this, we need to write out the mean value thoerem, which needs Rolle's theorem, which needs the extreme value theorem, which gets into the definition of the real numbers. As well as all the fun epsilon–delta arguments for the limit manipulations, of course. x/exp(sqrt(4x+3)) < x thankfully follows trivially from exp(sqrt(4x+3)) > 1 = exp(0). Since sqrt(4x+3) > 0, we just need to show that exp(z) is increasing. For this, we can treat the exponential as the anti-logarithm (since that's how my high school textbook did it), then show that log(z) is increasing, which follows from log'(z) = 1/z > 0 and our lemma. For log(x^2+1) < x, we'll want to use our lemma on f(z) = z - log(z^2+1) to show that f(x) > f(0) = 0. Here, f'(z) = 1 - 2x/(x^2+1), for which we need the chain rule and the power rule (or a specialized epsilon–delta argument). Since x^2+1 > 0, f'(z) > 0 is implied by (x^2+1) - 2x > 0, which luckily factors into the trivial (x-1)^2 > 0. So ultimately, we break the lemma up into (0,1) and (1,x) to avoid trouble with the stationary point. The trouble with problems like these is the whole foundation that the obvious lemmas have to be built upon. "Just look at the graph, of course it's increasing" isn't a rigorous proof. Of course, if you want to do this seriously, then you go and build that foundation, and on top of that you probably define some helpful lemmas for the ladder of asymptotic growth rates. But all of the steps must be written out at some point or another.