Hacker News new | past | comments | ask | show | jobs | submit | impendia's comments login

(Math professor here)

What do you mean by "foundational"?

I love Calculus Made Easy, but in my opinion the reason it's so good is that it doesn't try to be foundational. It relies on quick and dirty tricks -- especially, treating dy/dx as a fraction when it can't be formally defined as such, but where doing so makes the subject much more intuitive and easy. It's not really a good foundation for further study, you need something that doesn't cut corners for that, but it's fantastic for what it is!

My favorite foundational book is Linear Algebra by Jim Hefferon:

https://hefferon.net/linearalgebra/

It is free, and I've seen the author on HN occasionally. It's foundational in the sense that it builds up the subject brick by brick, assuming the minimum realistic prerequisites needed, and it does an outstanding job of this.

But it's a slow read, essentially by design. If you want something quicker, you might try Interactive Linear Algebra by Margalit and Rabinoff:

https://textbooks.math.gatech.edu/ila/

Again free, with lots of widgets to play with.

Some other textbooks I really like:

Epp's Discrete Mathematics is fantastic. The newest edition is astronomically expensive, so go looking for used copies of previous editions.

Carter's Visual Group Theory is tremendous fun. Once again not foundational per se, but if you want to learn what group theory is all about without slogging through lots of formalities, that's a great choice. I'd say that roughly it's in the spirit of Calculus Made Easy.

Also, if you enjoy poker, check out Dan Harrington's books on the subject. In the course of explaining hold'em strategy, they will teach you lots about probability, counting, expected value, and game theory in an applied setting. They're fantastically written.


> 12) Join a community of people sharing your struggles.

If you can't find an in-person one, the Reddit community is pretty good, with lots of useful posts and advice

https://www.reddit.com/r/ADHD/


> you can say "Outlook is shit" all you want, the users will blame you for it, since you weren't able to fix what others could, for better or worse.

Personally, I'd happily blame Microsoft, but the practical significance of this fact is nil.

I am in the very small minority of users who will sometimes complain to our IT when Microsoft forces shit down our throats. But I do this because it feels good, not because I imagine any realistic probability that doing so will make a difference.


For the same reason that people expect car infrastructure to be paid for: whether they are walking, biking, or driving, they are frequently traveling to some place where they will contribute to the economy.

Walking is not merely some sort of hobby. It is transportation, a means of getting from one place to another -- often the most convenient and pleasant means. And transportation infrastructure certainly falls under the purview of local governments.


There are strict privacy laws (e.g. FERPA) which university administrators are terrified of violating and getting sued over.

Meanwhile, most university "enterprise" software is a festering pile of shit.

I'm very surprised by the extortion attempt, but sadly a massive overreaction doesn't much surprise me.


Something I have noticed about higher education admins is that they hire consultants to do every project

I came to understand that this is because the career positions have such great benefits, often the last bastion of pensions, that these people literally go there to die.

So they take no risks and don’t try anything. They hire a consultant and if it doesn’t work out the blame lies there.

They also get big budgets to implement the consultant solution, which is bloated and terrible, so the department head gets more money every year to support it


I'm a university professor, and this is batshit crazy.

Who? As in not "they" or "the university", but who within the university? Can you tell where the directive is coming from?

If this comes from, say, the Provost's Office then this probably can't be handled internally. (The position of Provost is the #2 position at a university, and the provost usually runs the show while the President or Chancellor goes schmoozing with donors.)

But if it's coming from the Registrar's Office, then the Registrar doesn't have that much power internally, and you might be able to fight this decision within the university. What they did is not only brazenly immoral, it is also a tremendous legal liability for UW, and it should and might be a firing offense for whoever is responsible. And quite frankly no matter what happens I would seriously consider hiring an attorney (you might find one who will work on contingency).

You might speak with any professors in the department you have a good relationship with; I would be very surprised if they were sympathetic to this decision.

You might also talk with the university ombudsman, Dean of Students, etc. -- although I would be a little bit cautious and polite here. Just calmly describe the situation and ask what you should do in this situation. Hopefully (but this is very far from certain), they will calmly offer to intervene on your behalf, and then they will go ballistic behind closed doors and absolutely rake the Registrar over the coals. In any case, be poker faced, don't fully trust them, and avoid committing to a particular course of action if you don't have to.

Finally, here's an amusing hack. Salaries at UW are public record. If you want to find out how important any individual person is in the hierarchy, look up how much money they make. It's a fairly accurate barometer.

https://fiscal.wa.gov/Staffing/Salaries

Universities are not monoliths, and the relationships between different power centers are usually mistrustful at best.

Best of luck to you.


Are those numbers a sum of the total benefits or something? It seems insane that a campus security guard is making 170k.


It's total pay without benefits. It includes overtime and on-call time (which are typically paid at a higher rate).

It wouldn't surprise me that an experienced security guard is making $170K; the state itself is expensive, and they have to retain staff. The staff is often ex-cop, and guards very frequently work overtime (paid time-and-a-half or more). The guard may be a people manager (I don't know which row you're referring to but it looks like the typical guard makes far less).


I don't know.

I knew that salaries at public universities are public in many states, so thought to google it -- but the details can vary.


Consider the liability to which a bad security guard can expose your organization! Not that pay guarantees quality but still


It seems insane that you need campus security guards at all oO


A lot of campuses have actual police. In some ways campuses are similar to a municipality and have many of the services that entails (fire, trash, water, power, snow removal, parks, and security/law enforcement).

You could similarly ask why a town of 50,000 people needs a police department.


When you put it in terms of total number of people...it does make sense. A lot of universities down here in Texas have a small town+ amount of students and faculty and they tend to have their own police departments and other services.


My university had a police department because it is, as one might expect of a flagship state university, an enormous landmass with billions of dollars in infrastructure and equipment, plus about 6,000 full-time residents living in university-owned housing. Residents of a certain class of people who are prone to doing stupid, illegal shit.


Why?


Because police is a thing?...


Having worked in university administration before I would say that anyone who lasts as a manager is a professional politician, so expect them to have engineered a very good reason and possibly have allied with another department.

As manager pay is usually based on headcount instead of being aligned with good outcomes, they might just have threatened someone's mortgage payments. So, that manager might be willing to call in every favor and fight with everything they have got.

But yeah of course it's possible that they got into more trouble than they can handle.


The head coach of football gets paid $4mil a year (4x the president) and is the highest payed employee. The top 7 staff are all sports related.

Is this, like, common in the US? It seems batshit insane to an outsider.


A college like UW may have sports revenue on order of $300M, much of which goes to the university, and means students may pay less than if there were no sports. Dig carefully through UW finances, which are usually public record. Paying a coach whose program is a massive profit center enough to have a team of quality enough to land bigger TV deals may be a financial benefit.


I always see people saying that sports is financially positive on its own, but my actual experience is a ~10% tuition hike to subsidize sports expansion, so ...


Without knowing how much sports revenue offsets tuition, which I just showed you how to investigate, your 10% anecdote from millions of college students is irrelevant. It’s both possible sports offsets your tuition by 30%, and later you saw a 10% raise, but until you compute that initial offset your 10% gripe is meaningless.


My university's athletics program pulls in so much money and some of it funds academic programs. No money goes from academics to sports.

So the athletics department is not only self-sustaining and self-funding, but it funds academics as well.

It's basically as if Man U sent some of its profits to Manchester University.


Very common at larger state universities that have been around a long enough time to have a significant sports following.

It makes sense if you do the math.

Newer schools and smaller schools, typically not so much.

A lot of what we do in the US probably sounds batshit insane to outsiders so no worries about that and thanks for asking!


Universities in the US administer the main second-tier sports leagues for basketball and football, so yes, it’s common (though strange, I agree).


Yes, this is extremely common.

On the one hand, yes, this is absolutely batshit insane.

On the other hand, college sports are enormously popular; football games regularly play to sold out crowds of over 50,000, and during football season there will be games on TV all weekend (not just local ones). They bring in a lot of revenue and publicity for the university -- and the latter (debatably?) helps attract students to apply.


I'd never considered that a sports program could be revenue producing. That's quite interesting. Although it seems weird that higher education and (almost-professional) sports are so tightly coupled.


An interesting outsider perspective is this clip of Steven Fry going to an Auburn game: https://youtu.be/FuPeGPwGKe8

Regarding the latter, it’s weird and certainly was exploitative when college athletes weren’t allowed to monetize through sponsorships and frankly still is exploitative.


I was more thinking that there's not a particularly natural overlap between sports and academic ability. You'd think that by tying the two together, you'd get both worse sporting and academic performance than if they were unrelated.


The US has a decidedly liberal viewpoint on education. Sports ability is in some sense an educational endeavor. The ancient Greeks called it "athletics".

So US educational institutions don't really have any hangup against treating sports any differently than they might treat a CS class.

They are a subject you have to study and train at...and sometimes sit in a theatre and have a class time about (watching scout footage or deconstructing plays, etc).

Sports are probably just as rigorous as anything else academically once you get to something approaching a division 1 level of play. The reason we don't recognize it is because we suck and are mostly casual about it on a forum like this (filled with sports failures like myself or sports non-participants). The people actually in these programs with D1 scholarships and whatnot I guarantee take it as seriously as you or I would take calculus.


I never meant to imply that athletics wasn't a serious pursuit. I agree that physical capability is part of being a well-rounded person. It's certainly common here (Aus) for schools and universities to have sports teams and to strongly encourage participation.

What I find strange in the US context is the emphasis on it as a (revenue generating!) spectator sport. I understand that amateur (for want of a better word) sports can be highly entertaining; what I don't understand is why you'd go to university teams to find the best amateurs. I've played and watched enough sport to know that it's common for academic and physical abilities to be not particularly well correlated, particularly at tails of the distributions.


This is hardly an American phenomenon. The Bauhaus was famous for incorporating athletics too.


Not really. You can’t major in playing sports, you can’t get credit for it, and i don’t know what you mean by “as rigorous as anything else academically”, but it’s probably not true. I didn’t play division 1 anything but I did play in college (no scholarship).


It's batshit insane either way in the grand scheme of things. It just goes to show how market forces don't necessarily incentivize the things we actually want or need.


It seems like crowds of 50,000 people want this enough to regularly pay for it, subsidising other people’s education in the process.


Yes, and not just at public universities.


As a math researcher, and a signatory to the Elsevier boycott, I am confused. Not by the resignation itself, but rather by what Elsevier is attempting to accomplish.

From the resignation statement, linked to in the article:

> In 2023, Elsevier unilaterally took full control over the JHE EB scientific structure and composition through their requirement that all JHE AEs be recontracted annually. This action runs counter to their assurances that AE contracts would not undermine our longstanding principle of exercising editorial control of all scholarly decisions, including recruitment and retention of the expertise necessary to oversee the review process. (...)

I had believed that Elsevier's business model was to collect golden eggs for as long as we the geese were willing to lay them. Seems to have worked out quite well for them so far.

Why is it potentially in Elsevier's interest to reach more tightly for the reins? Is this just executives being clueless, or is this some kind of clever financial strategy which I'm failing to appreciate?


What every public business exec wants. More money short term. They have zero concept of long term strategies at this point.


Having lived in Japan, there is something of an attitude there that anywhere other than Tokyo -- or maaaaaybe Osaka if you're feeling generous -- is the sticks.

Having been to Sapporo and Kumamoto -- and many other medium-size Japanese cities -- this attitude can seem awful silly when you're walking around their downtowns. But it can be a self-fulfilling prophecy: if people in charge of "opportunities" leave for the biggest cities, then that's what matters.

Indeed, on my trip to Kumamoto I was visiting a fellow academic, and when I got there he told me he was trying to move so he could be closer to his family in Tokyo. He has since moved to Nagoya, and apparently is happier there.


I think people like medium-size cities in general. Kumamoto in particular is attractive, is decently convenient, good climate, and while Kyushu in general has a conservative image ("Kyushu danshi") it has been changing for the better.

But given all of that, Tokyo basically has its own economy, it's own rules, and isn't just "big", it works differently enough that people's choice isn't on which city, but whether they live in the Tokyo area or not.

For instance if you're gay, the Tokyo administration will give you an equal marital status. Kids's private school tuitions are partly covered (they're ragingly expensive in the first place, but you get prime access to very competitive schools). Health care will usually be completely free for kids. Remote working is usually treated differently if you're vaguely in the area or if you need a flight, living in the mountains in Okutama will land a better deal that living in Shizuoka, even if commute wise it's probably the same.

This is of course an issue, especially as national policies need to fit both worlds which is a pretty hard (the whole discourse on the spouse wage limit is basically centered on this divide)


People go to Tokyo and Osaka because that's where it's easier to find good-paying jobs.


I'm 46, and I've gone through something of a midlife crisis recently (and things are getting better now!)

When I was a kid, I was constantly being told how much much "potential" I had. I have accomplished a lot, and when I was in my twenties and thirties it was easy to imagine that all the things I hadn't accomplished yet were still ahead of me.

Now, I've been faced with a reckoning: for sure, many great things still lie ahead, but I won't be able to achieve all of my aspirations.

One thing that worked for me: seek professional help. I sought out a therapist and am still working with her. When I developed insomnia, I tried pretty much everything (medication, CBT, sleep study etc.) until I eventually found a medication that worked. This took years, but things are better now.

Also, avoid the "sunk cost" fallacy. For years I practiced at a yoga studio which was excellent, but the vibe was a little bit off for me and I wasn't enjoying myself. I just sucked it up and kept going. But after Covid I decided to try something different, and ended up finding group fitness classes which I love.

Good luck!


Just curious, what kinds of group fitness did you end up enjoying? Asking as someone who formerly spent a few years doing yoga too.


Cross training -- a mixture of cardio and strength training, with weights, rowers, kettlebells, battle ropes, medicine balls, etc. etc. and all sorts of calisthenics -- something different every day.

It's not a chain establishment, and overall I really like the owner/head trainer and the mood he sets. I'm living in a town that's a bit too laid back and slow-paced for my taste overall, whereas this guy acts like he has twenty cups of coffee every day -- while managing to remember everybody's name and coming around to help you if you're having difficulties.


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 specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer.

Here is an elementary example, which could be worked out by anyone with a good background in high school math. Prove the following statement: 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.

i.e. the left-side is big-O of the right.

This flavor of statement comes up all the time in analytic number theory (my subject), would be regarded as obvious to any specialist, and in a paper would be invariably stated without proof.

To come up with a complete, rigorous proof would be long, and not interesting. No professional would want to read one.

I agree this attitude comes with some tradeoffs, but they do seem manageable.


> 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.


> 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.


You might as well have written that mathematicians should stop doing mathematics. If every mathematician were to work full time on formalizing theorems in proof assistants, then no living mathematician would ever do original research again -- there is simply too much that would need to be translated to software. And to what end? It's not as if people suspect that the foundations of mathematics are on the verge of toppling.

> Code is easy to share, easy to collaborate on [...] collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff

Here's an experiment anyone can try at home: pick a random article from the mathematics arxiv [1]. Now rewrite the main theorem from that paper in Lean [2]. Did you find this task "easy"? Would you go out of your way to finish the "tedious" stuff?

> even horrible code is far better at documenting what it does than what you are describing

The "documentation" is provided by talking to other researchers in the field. If you don't understand some portion of a proof, you talk to someone about it. That is a far more efficient use of time than writing code for things that are (relatively) obviously true. (No shade on anyone who wants to write proofs in Lean, though.)

---

[1] https://arxiv.org/list/math/new

[2] https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...


> 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)


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.


> 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.


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.


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.


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.


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.


> 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.


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.


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.


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.


I think Kevin Buzzard et al are aiming for a future where big, complicated proofs not accompanied by code are considered suspicious.

I wonder if being able to drill all the way down on the proof will alleviate much of the torture you mention.


Using vague terms like "obvious" or "standard techniques" is doubtless wrong, but I would not see any problem in a paper basing its conclusions on demonstrations from a source listed in the bibliography, except that in many cases those who read the paper are unable to obtain access to the works from the bibliography.

Even worse is when the bibliography contains abbreviated references, from which it is impossible to determine the title of the quoted book or research paper or the name of the publication in which it was included, and googling does not find any plausible match for those abbreviations.

In such cases it becomes impossible to verify the content of the paper that is read.


This is a wider problem in general and an odd bit of history: scientific papers pre-date the internet, and as such the reference system exists pre-computation. the DX-DOI system is a substantial improvement, but it's not the convention or expectation - and IMO also insufficient.

Realistically, all papers should just be including a list of hashes which can be resolved exactly back to the reference material, with the conventional citation backstopping that the hash and author intent and target all match.

But that runs directly into the problem of how the whole system is commercialized (although at least requiring publishers to hold proofs they have a particular byte-match for a paper on file would be a start).

Basically we have a system which is still formatted around the limitations of physical stacks of A4/Letter size paper, but a scientific corpus which really is too broad to only exist in that format.


The issue with hashing is that it's really tricky to do that with mixed media. Do you hash the text? The figures? What if it's a PDF scan of a different resolution? I think it's a cool idea—but you'd have to figure out how to handle other media, metadata, revisions, etc, etc.


DOIs fix that.


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.


> (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.


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).

I think this practice happens in many specialized fields. The thing with math is that the main problem is the publications become inaccessible. But when you have the same sort of thing in a field where the formulations assumptions that aren't formalizable but merely "plausible" (philosophy or economics, say), you have these assumptions introduced into the discussion invisibly.


Not a (former) mathematicien (but as a former PhD student in theoretical physics still some affinity with math): I remember being shocked when, having derived a result using pen and lots of sheets of paper, my co-promotor told me to just write '<expression one> can be rewritten as <expression two>' and only briefly explaining how (nothing more then a line or two), as the magazine we were to publish (and did publish) the article would not want any of those calculations written out.


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.


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.


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.


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.


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.


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).


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.


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.


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.


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.


>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.


"the proof is trivial"

"but can you prove it?

[10 minutes of intense staring and thinking]

"yes, it is trivial"


I didn't learn big O at high school though.


Calc AB covers it, and BC certainly gives you enough for a proof.


Join us for AI Startup School this June 16-17 in San Francisco!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: