quasisphere

(Sorry for the long post, but yours brought me thinking about a bunch of different aspects.)

First of all, I did not mean to downplay elegance at all. I agree that elegance is very important and that math is very much about trying to find elegant ways to think about various problems and phenomena. It also makes math feel more human and art-like, as elegance is not completely objective. And I also agree that LLMs do not seem to currently have consistent mathematical taste. I find they often do quite ugly or unoptimal proofs, although sometimes they also surprise me with a more elegant one than what I had in mind myself. And when we pass from arguments to choosing good definitions or seeing the big picture they are often much worse. Finally, formalization efforts such as Mathlib are very interesting from the elegance point of view. I'd actually be interested to see whether it would be possible to do lecture notes or textbooks based on Mathlib, written in standard math prose so that wider crowd of mathematicians might benefit from the insights that people had while formalizing.

However, as a research mathematician, I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems. These formalized versions are at least at the moment not going to have pretty proofs, and the proofs the LLM comes up with might even be different from what I'm writing in the paper (but probably in practice not very different if I'm formalizing every lemma). Still, if this can be done quickly enough, I think the result could be net positive even if the formalizations never leave my local hard drive: I will have confidence that I did not miss an edge case in the statements, where usually double-checking these things is actually a very time-consuming part of writing a paper. Thus I might be able to produce papers with less mistakes (usually non-important ones but they do happen). In this sort of workflow speed matters, and if you need a particular prerequisite theorem from the end of a textbook, you'd rather do it faster than half the reading speed (that's impressive by the way, and I do not mean this sarcastically!).

Returning a bit to the topic of elegance, I'd also like to claim that the elegance of arguments is probably at least as important as the elegance of definitions. And if you find an elegant argument, later on that might serve as a basis of a definition. There might also be some difference in how well this works out in practice in different fields. At least historically people in analysis (like myself) are happy to repeat known arguments in slightly different settings. It could be hard to make a version that works in every setting because different sets of assumptions could allow for a similar argument to work. Or it could also be easier to just remember the actual technique rather than trying to give it some jargonish name. Anyway, as I said above, I think LLMs are a bit better with arguments than definitions, so some elegance might be retained and perhaps you can later refactor to use more elegant definitions as well. (Hmm, a random idle thought, but a refactor from arguments to specific theorems could be in some sense similar as going from an untyped or not-explicitly-typed programming language to a typed one so there might be a coding analogue here as well.)

Finally, thanks for bringing up the limitations of LLMs. I also feel that LLMs are probably not currently able to really go beyond their training data, producing new theories with truly novel arguments or definitions. I'm skeptical that we will see a proof of the Riemann hypothesis in near future just drop from an LLM (human utilizing an LLM could be a bit of a different story, but I'm not a number theorist and have no idea whether anyone in the field has any plausible attack vectors currently). They are getting very good at combining and rephrasing existing stuff, however.

I actually noticed after I posted that I should have said 'by individuals at pace not too different from writing down a standard prose proof' or something similar to address this point. Mathlib for instance is of course a phenomenal project, but it was written by a large amount of people over many years. Granted their goal was not so much speed as it was elegance, but by 'viable' I had in mind something that a research mathematician could actually use in real time along actual math research. The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that, both individually and collaboratively (such as the recent Tau Ceti project).

Anyway, what do you mean by 'say it's a proof of something'? If you mean this in technical sense, there are plenty of examples around where single individuals or small teams have autoformalized theorems with tens or hundreds of thousands of lines Lean code that pass a comparator challenge (so the theorem is correct). If you mean this in the sense that the proof is also a proof in the eyes of humans, so that someone has actually read or understood the proof, I'm willing to acknowledge that in this area there is much work still to do. In my own experience the current LLMs are already very strong at formally proving theorems (with correct semantics), but they are still lacking in writing human-readable math prose based on these formalizations, for instance.

Agreed. In addition I think a big reason why we are discussing formalization so much at the moment is that it has only recently become viable to do large scale formalization of mainstream mathematics, using LLMs. These same LLMs will make it much easier to translate from one language to another and port even larger codebases over.

My prediction would therefore be that the LLMs will let us work more-or-less using standard mathematical prose that then gets to codified to some machine-readable and checkable language, but what the language used by the proof checker actually is will be more of a technical detail. In particular, I suspect people will not care too much about the language used for proofs themselves, which means that we might allow for more boilerplate if it is faster to elaborate/compile, unlike current interactive theorem provers which are meant to ease the work of humans. How the language looks like for the statements of the theorems and definitions is probably more important however, since humans will want still to be able to check that what is being formalized corresponds to what they had in mind.

Thanks for sharing, this was interesting to read! I wonder if the approach in the "How to win clone wars" section would also work to limit the number of accounts one can have on a given service (the article seems to rather consider rate limiting). It would be refreshing to have a forum where everyone is guaranteed to have at most 1 (or perhaps 2, say one anonymous and one with your name) account that is also backed by a unique government ID (without disclosing to the government your account or even that you have one). This could help a lot with the bot spam and trust issues.

Just to make sure that people understand the clarification correctly: This is about upstreaming the work by Asahi Linux team. In particular, Linux on Apple Silicon macs is quite usable already if you use their own Arch-based distribution which includes yet-to-be-upstreamed patches. I run it on my M1 Air and the only major (to me) things with no support yet are the builtin speakers (afaik support is coming soon) and the webcam.

Here's sketch how to construct such a function: Let's start by defining f on Q (the rational numbers) by first splitting Q into countable number of disjoint dense subsets A_n of R (e.g. look at reduced fractions whose denominators are of the form p^k for some prime p, for fixed p every such set is dense and for different p's they are disjoint). As rationals themselves are countable, we may then set f(x) = q_n for all x in A_n, where q_n is an enumeration fo the rationals.

This construction already gives us a function such that every interval (x_1, x_2) contains a point x such that f(x) = y for every rational number y.

Now, in a similar way we may consider a set of the form s + Q where s is an irrational number. Setting f(x) = s + q_n for all x in s + A_n, we get a function which also attains all numbers of the form y = s + q for some rational q on every interval.

Finally, let's say that two real numbers s and t are equivalent if they differ by a rational number. By the axiom of choice we can choose a representative from every equivalence class, so that for every two representatives s and t the sets s + Q and t + Q are disjoint. Using the above construction for every representative lets you define a function with the property you wanted.

338 * 2 = 676, which is between 440 and 880

I think what could be worth exploring is progressive energy taxing. Basically let each individual consume a certain amount which is needed for living a normal life, but tax energy usage exceeding that increasingly heavily.

On top of this base model one could then also introduce subsidies for specific energy intensive industries that are deemed essential (probably not bitcoin).

That would handle the distribution of limited* amount of energy we have. CO2 emissions should probably be taxed separately and progressive rates would seem reasonable to me here as well.

* Yes, we can still build more, but at some point the energy usage has to stagnate. Exponential growth in usage would lead the Earth to become very hot in a few hundred years since the only way heat gets released to space is via infrared radiation which is limited by the surface area of the planet [1, Section 1.3].

[1] Murphy, T.: Energy and Human Ambitions on a Finite Planet (2021), a free textbook at https://doi.org/10.21221/S2978-0-578-86717-5

Perhaps a bit misleading title since the predictions were mainly (with a few exceptions) about the future of music industry instead of music itself.

It is an interesting question how much music itself can advance while still staying enjoyable by a significant number of people. For instance much of the popular music nowadays appears to be rather simplistic in terms of rhythms and harmony, and the innovation has been happening more on the timbre.

In classical music more modern approaches such as atonality never seemed to gather such large scale interest as the stuff from older masters. Time will show if e.g. microtonal music will make a breakthrough at some point, but it is hard since the new harmonies sound just 'wrong' until the listener learns them. (Of course for some native listeners the same could presumably be said about western music.)

I guess it's not a completely unreasonable guess to say that there are some optimal thresholds of complexity for a human brain and that's why simple regular clapping and singing in thirds and fifths will continue to evoke the strongest emotions for the majority of people.

I think one aspect of climate engineering that I don't see discussed very much is who is allowed to do that: Is a single country permitted to make decisions that affect the whole globe? Who decides how hot/cold the earth should be?

Just as an example, some African countries could decide that in fact they would like to make the climate even colder than it used to be, which on the other hand would negatively impact agriculture away from equator. I think these questions form a big potential source of global power struggle and conflict.