generationP

This is nice, but I suspect that a barycentric coordinate bash with the formulas in Evan Chen's book could also do 30% of the IMO (seeing that most of it is about triangles) on a modern laptop.

I expected three-number inequalities to give in first, as there is less of a question about what counts as a proof. I didn't know that the latter problem was already solved in 2000 ( http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf ).

Someone really should make an adventure game out of synthetic geometry, as it allows for a proof-writing language simpler than Lean's and allows for nice visuals.

Ah, thanks! It seems to be this one http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf plus some algebra for adding angles and lengths. As I hoped, they are using oriented angles mod 180° ("full-angles") to get rid of betweenness conditions. They are also using evaluations at rational (I think) coordinates to check that nondegenerateness conditions are satisfied when the data is in general position. This is not as nice as I had hoped for, but certainly no worse than what contestants do at the IMO. And because a bunch of methods are off-limits (congruence criteria, probably anything involving undirected unsquared lengths), I'm not surprised that their proofs are longer/slower than human ones -- they're better proofs.

What they did here is one of the first steps towards an AI that generates nontrivial and correct mathematical proofs. (An alternative benchmark would be IMO-level inequalities. Other topics such as algebra, combinatorics and number theory are probably no easier than the rest of mathematics, thus less useful as stepping stones.)

And an AI that generates nontrivial and correct mathematical proofs would, in turn, be a good first step towards an AI that can "think logically" in the common-sense meaning of the word (i.e., not just mess around with words and sentences but actually have some logical theory behind what it is saying). It might be a dead end, but it might not be. Even if it is, it will be a boon to mathematics.

What deductive system are they using to verify the proofs? I'm asking because the conventions of olympiad geometry are slightly different from those of the rest of mathematics (you can make informal "general position" arguments; you can pooh-pooh issues of sign and betweenness; you can apply theorems to unstated limiting cases; etc.), and it is far from obvious to me how this logic can be formalized without causing contradictions.

> humanly navigable

This is Sweden; I would bet that there are hiking trails connecting everything on that map, although maybe not a single one for all the planets. Roslagsleden (13 day hikes) + the first 9 etapper of Vikingaleden bring you from (close to) Mars to Uranus. And these are some nice hikes:

https://www.roslagen.se/roslagsleden

https://www.roslagen.se/vandra-vikingaleden

> The video content industry has Kafkaesque licensing agreements

Isn't the same happening with video games? I've seen video games remove some music from their soundtracks as their limited-time licenses lapsed.

Interesting! So that's why I used to get crappily rasterized printouts of PDFs in Chrome a few years ago.

I had thought printers could be trusted with their own rendering, but of course that is another can of worms...

Learning a language at school, you will soon be better than natives at grammar. It's the vocabulary, idioms and implicatures that will be tripping you up. Does grammarly really help with those?

Huh? How does a video card affect printing?

Yep, but that's begging the question :)

Do we know what messages were the bone of contention? Don't tell me this isn't common knowledge among dozens of people at least...

Ah, IRC. Yeah, I came too late to make new friends there (though it was still good for keeping in contact with old ones). Still managed to enjoy the usenet, although the "big" groups were already full of spam.

How much was there to find on the internet in the 90s?

I arrived ca. 2001 and found enough high-quality content (folk songs, math puzzles, some books already digitized) to feel like I had discovered a giant library. And it kept growing: Wikipedia arrived, various forums and magazines appeared (most were crap, of course, but there was no shortage of good ones).

As far as I can tell, things started getting worse around 2008, with places such as geocities closing down and social networks rising; then the deprecation of Java and Flash kicked the floor out of some of the good old parts. Other things were still improving, though, up to 2015 or so. It's only recently that I see most "culture production" locked in perennial closed gardens with unaccountable moderation. I wish I could point to some places still on the rise other than arXiv and LibGen...

What had I missed from the 90s that didn't make it into the 00s?

4th edition and still hasn't bothered to disambiguate between polynomial and polynomial function.

Still a good example of mathematical writing. But, as Einstein supposedly said, "as simple as possible but not simpler". Why is it always American authors that forget that last part?

It seems to have a bug where if you load a file from the app using the quick-load 1,2,...,10 keys in the File menu, then the next time you open another file in SumatraPDF from the explorer, it immediately opens several other files. This may be related.

This is more trouble than it's worth for the mathematicians of today. What exactly is gained from these ORCIDs? A DOI auto-generates a clickable link, allows for automatic reference tracking, and (hardly an intended feature but perhaps the best one) helps readers find a copy in places like sci-hub and LibGen (on sci-hub, DOI is the only lookup option that currently works). With an ORCID, I could make it double-clear that the D. E. Knuth I'm citing is the real Donald Ervin Knuth. Nice, but I'm supposed to learn a new command and spend 10 minutes researching authors per paper for that?

OK, so I typically use DOIs in my bibliographies, although I seem to be in the minority for now. What next? You have to find the exact name of the author that changed and edit it. Let's say you do so (not a trivial undertaking since references do not come in a standardized format even if the DOIs do; by the way, arXiv doesn't understand bibtex). Now my paper says "Merton and Fox observed in [5] that...", and you know that Fox (one of the authors of the [5]) became Wolf. Will you change my text to "Merton and Wolf observed in [5] that..."? How can you tell that this particular "Fox" is a surname rather than the animal? What about acknowledgments, which come with no DOI or ORCID?

SumatraPDF on Windows is lightning fast with the kind of PDFs you get from the arXiv (true PDFs without heavy graphics). I don't know what is fast on Linux, but probably some MuPDF-based viewers are (the MuPDF PoC viewer is fast even on WSL).

Huh, not half bad! Reporting a few bugs.

Though that one is perhaps to blame on pdfTeX rather than on the TeX format :)

They seem to be trying:

> In addition, arXiv will provide substantially better access to the visually impaired by producing HTML as well as PDF versions of its content.

But it's a different question whether they will succeed. A compile-to-HTML pipeline needs to work with every single LaTeX package that people use, or at least work with most ones and fail gracefully for the rest. That was hard enough for compile-to-PDF, requiring the arXiv to keep every year's version of TeX Live permanently maintained.

There is no good way to deal with name changes. You can change them in the metadata, but the old ones will still be around in the paper itself. You can let authors change them in the paper, but the old ones will still be around in others' bibliographies. You can't do much about the bibliographies, since (1) you'd need an automated way to find them all and disambiguate them (have fun with Chinese names) and (2) a lot of authors will reject the idea that someone else changes their papers.

Browsers are painfully slow at rendering PDF. Open them with your local reader.

That'd be good.

> migrate to the cloud

Oh great, looking forward to a captcha every time I download a paper.

(FWIW, arXiv is one place I trust not to make such stupid decisions, but migrating to a cloud often means the decisions are no longer made in-house...)

The omnibox stayed but got nerfed in a rather idiotic way, if https://support.google.com/chrome/thread/6240767/behaviour-o... is to be trusted. So I wouldn't say it "never happened", assuming that this is what they were talking about. But apparently it's back to the correct behavior now (and has been for a while).

Could it have been what led to this? https://support.google.com/chrome/thread/6240767/behaviour-o...

Ah, I didn't spot that they no longer require counting installs. But you're right; this is probably what "the number of new people" means. And the "2.5% revenue share" variant means no hurdles for freeware. So a real improvement indeed. Thanks for the corrections!

[EDIT: False; see comments.]

From a viewpoint of "will it be compatible with a DRM-free release that doesn't phone home" (i.e., playing by GOG rules), this doesn't seem to solve the problem at all. What is in it for them? Why per install and not per sale?