jules

They are using a Lean tool where you separately state your theorems with `sorry` and then prove them elsewhere. The tool checks that all sorry's are covered. This is so the AI doesn't need to edit the specification of the theorem statement.

If there is any country that can safely build nuclear power plants, it is Switzerland.

I was robbed at a gas station in Jersey City and the police retrieved the airtagged backpack in 20 minutes. The police was fantastic.

I think it would be more effective if US establishes deterrence against punitive fines of its companies.

The are fining his company 213% of yearly Italian revenue. He is not the one escalating.

If Italians have no influence over AGCOM, then who does?

I don’t see what the benefit of most of that is, and why publication fees are a good way to pay for it. Take video recordings: why should we pay for them to develop a video hosting platform when perfectly good ones exist? In fact, conferences that I am familiar with put the recordings on YouTube, and this works great.

> ACM has to be careful to not get into financial trouble by giving away their crown jewels without generating sufficiently stable alternative income sources.

The attitude that the work of science belongs to these publishers is what grates me the most. Yes, ACM is not as bad as Elsevier, but this attitude is still fundamentally wrong. They are in the position they are mostly by historical accident, able to extract rents because it requires a lot of coordination to switch.

Why do I call it rent extraction despite the ACM doing stuff? Suppose the ACM charged separately for using their video platform. Would anyone pay for that?

> For example, authors no longer generate their own PDFs but submit the LaTeX/Word manuscripts to a central service (TAPS), developed and operated for ACM by an Indian company, Aptara

And what good is that? Why should we pay for a separate company to run pdflatex for us? The system exists primarily to check that we’ve put ACM branding in the paper.

Sometimes people also say that the real service is long term storage of pdfs, but let me preempt that right now: there are government sponsored long term storage facilities like Zenodo that are likely to outlast ACM. Second, commercial storage paid for indefinitely using an annuity would cost less than $1 in present value for hosting the pdfs of a conference, about 0.0001% of ACM publication fees.

The peer review is all done by volunteers of conferences, not ACM.

That isn't the case. Conferences organize their own website to submit articles for review. Volunteers from the conference pre-filter submitted articles for spam, the rest is handled by the review committee. There is no cost to submit. In fact, the eventual cost is often not even mentioned at that point. When the article is accepted for publication, the conference gives authors a link to an ACM website where the authors upload their PDFs. Only after that will the authors be asked to pay the fee (and if you wanted, you could refuse at that point, which presumably means that the conference will eat the loss, or maybe they'll un-publish your article).

I don't think spam is a huge issue. The conference websites and submission portals are niche and random people don't tend to find them or care enough to go through the trouble.

This is good, but they're now charging authors a publishing fee of over $1000 per article (and they say that that is the discounted price). It is unclear whether this is justified. In my experience publishing scientific articles with ACM, all the real work (such as peer review) is done by volunteers. From what I can tell, ACM just hosts the exact PDF + metadata that authors supply. I suspect that in the future, more journals and conferences will switch to an arXiv-overlay model.

iPhone 17 pro max is balanced with their standard case.

3blue1brown actually shows the usefulness of formalism. The videos are great, but by avoiding formalism, they are at least for me harder to understand than traditional sources. It is true that you need to get over the hump of understanding the formalism first, but that formalism is a very useful tool of thought. Consider algebraic notation with plus and times and so on. That makes things way easier to understand than writing out equations in words (as mathematicians used to do!). It is the same for more advanced formalisms.

For another comparison: this is about 4 years worth of UK App Store net revenue.

What they are buying is support of the French.

That's the point, the regulation effectively locks in USB-C as it is.