12,368 karma · joined June 3, 2009
Cofounded https://flourish.studio; now exited & looking for the next big project
For me it was wonderful. I already knew how to write computer programs, as that's what I had spent most of my waking hours doing before that point, but learning how to think rigorously about the correctness of programs was a revelation to me.
See https://en.wikipedia.org/wiki/Writing_system#Linearity for more detail.
See [0] for an exposition, or [1] for a recent popular article about it.
0. https://www.wisdom.weizmann.ac.il/~oded/p_TreeEval.html
1. https://www.quantamagazine.org/catalytic-computing-taps-the-...
> Customers already using Advanced Data Protection, or ADP, will need to manually disable it during an unspecified grace period to keep their iCloud accounts. The company said it will issue additional guidance in the future to affected users and that it does not have the ability to automatically disable it on their behalf.
It’s also a clever device to make the account of the author’s visit more vivid, because I as the reader imagine making the journey myself.
(But I do think it would be a fun adventure to try to follow the directions.)
> The 1278 people who said they utterly loathed AI art (score of 1 on a 1-5 Likert scale) still preferred AI paintings to humans when they didn't know which were which
There’s also a good joke at the end:
> Marcel Duchamp famously tried to put a urinal in an art museum to challenge people’s view of what art was. The administration rejected it, but Duchamp had the last laugh: in 2004, a survey of art professionals judged it the most influential artwork of the 20th century. Art, it seems, is most meaningful when it challenges our very concept of what art is.
> By this standard, I submit that Sam Altman is the greatest artist of the 21st century.
> In Unicode the letter ℘ is given the codepoint U+2118 in the block "letterlike symbols", named "script capital p". But in fact it's lowercase.
Unicode technical note https://www.unicode.org/notes/tn27/ clarifies:
> Should have been called calligraphic small p or Weierstrass elliptic function symbol, which is what it is used for. It is not a capital "P" at all. A formal name alias correcting this to WEIERSTRASS ELLIPTIC FUNCTION has been defined.
In addition to this, there are Lex Fridman's series of interviews with various key people from Anthropic [0], and a long discussion between Stephen Wolfram and Eliezer Yudkowsky on the theme of AI risk [1].
If anyone really wants to nerd out on the rhombic triacontahedral die, my proof of uniqueness is at https://s3.boskent.com/rhombic-triacontahedron-die/uniquenes...
I first discovered the result computationally, using a program written in https://sentient-lang.org/, before finding the ‘human’ proof described in that PDF.
I suppose this is encouraging! It shows that the forces of openness are gaining ground in this battle.
Needless to say, it was rapidly shut down following threats of legal action by Royal Mail.
https://www.theguardian.com/technology/2009/oct/05/ernest-ma...
https://blog.okfn.org/2009/10/05/ernest-marples-uk-postcode-...
I take this as a reminder of the importance of giving precise names to variables. The code
res = await originalFetch(url, init)
url: URL | RequestInfo
It would have been more difficult to overlook the problem with this change if the parameter were named something more precise such as `urlOrRequestInfo`.
(A much more speculative idea is the thought that it is possible to formalise the idea of a value being “used up” using linear types, derived from linear logic, so conceivably a suitable type system could prevent this class of bug.)
[0] https://github.com/PostHog/posthog-js/pull/1351/commits/2497...
Since I think you need an account to read threads now, here's a transcript:
Google DeepMind have produced a program that in a certain sense has achieved a silver-medal peformance at this year's International Mathematical Olympiad.
It did this by solving four of the six problems completely, which got it 28 points out of a possible total of 42. I'm not quite sure, but I think that put it ahead of all but around 60 competitors.
However, that statement needs a bit of qualifying.
The main qualification is that the program needed a lot longer than the human competitors -- for some of the problems over 60 hours -- and of course much faster processing speed than the poor old human brain.
If the human competitors had been allowed that sort of time per problem they would undoubtedly have scored higher.
Nevertheless, (i) this is well beyond what automatic theorem provers could do before, and (ii) these times are likely to come down as efficiency gains are made.
Another qualification is that the problems were manually translated into the proof assistant Lean, and only then did the program get to work. But the essential mathematics was done by the program: just the autoformalization part was done by humans.
As with AlphaGo, the program learnt to do what it did by teaching itself. But for that it needed a big collection of problems to work on. They achieved that in an interesting way: they took a huge database of IMO-type problems and got a large language model to formalize them.
However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems.
It's not clear what the implications of this are for mathematical research. Since the method used was very general, there would seem to be no obvious obstacle to adapting it to other mathematical domains, apart perhaps from insufficient data.
So we might be close to having a program that would enable mathematicians to get answers to a wide range of questions, provided those questions weren't too difficult -- the kind of thing one can do in a couple of hours.
That would be massively useful as a research tool, even if it wasn't itself capable of solving open problems.
Are we close to the point where mathematicians are redundant? It's hard to say. I would guess that we're still a breakthrough or two short of that.
It will be interesting to see how the time the program takes scales as the difficulty of the problems it solves increases. If it scales with a similar ratio to that of a human mathematician, then we might have to get worried.
But if the function human time taken --> computer time taken grows a lot faster than linearly, then more AI work will be needed.
The fact that the program takes as long as it does suggests that it hasn't "solved mathematics".
However, what it does is way beyond what a pure brute-force search would be capable of, so there is clearly something interesting going on when it operates. We'll all have to watch this space.
The Linux server revolution was still a few years away (at least it was for us – perhaps we were behind the curve), so our webservers were all Sun Enterprise machines running Solaris.
We decided to use a server process that had an in-memory representation of the active users, which we would query using doors from a custom Apache module. (I had read about doors and thought they sounded cool, but neither of us had used them before.)
It worked brilliantly and was extremely fast, though in the end it was never used in production because of changing business priorities.
I would guess that quite a few HN readers are in the happy position of being able to spend $105 on an interesting book without suffering financial hardship as a result.
But in general it’s reasonably common for a proof to have been written up to the best of the author’s ability, and for it still to be impossible for anyone else to understand it well enough to be confident in its correctness.
Formal logic was no help, for two reasons. First of all the formal logical systems of the early 20th century were really a sort of existence proof, to show that a formal logical system can in principle be defined, and were too unwieldy and verbose for practical use in non-trivial situations. Secondly, it would then become necessary for the reader to check the correctness of a proof in formal logic, which is an even more difficult task than checking a well-written informal proof.
But this is changing: modern formal proof systems are designed with user-friendliness in mind, and produce proofs that can be verified by computer. It’s now starting to happen that formalisation can be used as a way out of the impasse where a proof is too complicated for anyone but the author to understand. I can think of two examples of this: Thomas Hales’s Flyspeck project [1] was the first such case, and required a monumental effort from Hales and his collaborators. Much more recently, Randall Holmes’s proof that NF is consistent was formalised [2], finally putting to rest a very old question in the foundations of logic.
1. https://arxiv.org/abs/1501.02155
2. https://www.logicmatters.net/2024/04/21/nf-really-is-consist...
The first paper in the series was posted to the arXiv yesterday. [2]
It’s obviously far too soon to say whether the proof is correct, but I’m sure experts will be taking a keen interest.
1. https://people.mpim-bonn.mpg.de/gaitsgde/GLC/ 2. https://arxiv.org/abs/2405.03599