I think the "sudden and inexplicable flashes of insight" description of Ramanujan is exaggerated/misleading.
On the first example of the post: It's not hard to see that the problem is, by the formula for triangular numbers, roughly(!) about the solvability of
.
Since is roughly a square - - one can see that this reduces to something like Pell's equation . (And if you actually do the calculations while being careful about house , you indeed reduce to .)
I think it's totally reasonable to expect an experienced mathematician to (at a high level) see the reduction to Pell's equation in 60 seconds, and from that making the (famous, standard) association to continued fractions takes 0.2 seconds, so the claim "The minute I heard the problem, I knew that the answer was a continued fraction" is entirely reasonable. Ramanujan surely could notice a Pell's equation in his sleep (literally!), and continued fractions are a major theme in his work. If you spend hundreds-if-not-thousands of hours on a particular domain of math, you start to see connections like this very quickly.
About "visions of scrolls of complex mathematical content unfolding before his eyes": Reading the relevant passage in The man who knew infinity, there is no claim there about this content being novel or correct or the source of Ramanujan's insights.
On the famous taxicab number 1729, Ramanujan apparently didn't come up with this on the spot, but had thought about this earlier (emphasis mine):
Berndt is the only person who has proved each of the 3,542 theorems [in Ramanujan's pre-Cambridge notebooks]. He is convinced that nothing "came to" Ramanujan but every step was thought or worked out and could in all probability be found in the notebooks. Berndt recalls Ramanujan's well-known interaction with G.H. Hardy. Visiting Ramanujan in a Cambridge hospital where he was being treated for tuberculosis, Hardy said: "I rode here today in a taxicab whose number was 1729. This is a dull number." Ramanujan replied: "No, it is a very interesting number; it is the smallest number expressible as a sum of two cubes in two different ways." Berndt believes that this was no flash of insight, as is commonly thought. He says that Ramanujan had recorded this result in one of his notebooks before he came to Cambridge. He says that this instance demonstrated Ramanujan's love for numbers and their properties.
This is not say Ramanujan wasn't a brilliant mathematician - clearly he was! Rather, I'd say that one shouldn't picture Ramanujan's thought processes as wholly different from those of other brilliant mathematicians; if you can imitate modern Field's medalists, then you should be able to imitate Ramanujan.
I haven't read much about Ramanujan; these are what I picked up, after seeing the post yesterday, by thinking about the anecdotes and looking to the references a little.
HCH is not defined in this post, nor in the link, about it.
For those reading who do not know what HCH means (like me!), HCH is a recursive acronym which stands for 'Humans Consulting HCH', an idea I think originating with Paul Christiano related to iterated amplification. It involves humans being able to recursively consult copies/simulations of themselves to solve a problem. It is discussed and explained in more detail in these two posts:
If HCH is ascription universal, then it should be able to epistemically dominate an AI theorem-prover that reasons similarly to how Ramanujan reasoned.
My guess is that HCH has to reverse engineer the theorem prover, figure out how/why it works, and then reproduce the same kind of reasoning. This seems plausible to me but (if this is what Paul has in mind too) I'm not sure why Paul assumes HCH to be able to do this quickly:
Moreover, I’ll assume that it’s universal with some small blow-up, i.e. that if we give HCH a budget k N, then it epistemically dominates any computation that could be simulated by HCH with budget N.
It seems to me that it could easily take a super-linear (or even super-polynomial) budget to reverse engineer how a computation works since it could require disentangling opaque and convoluted algorithms, and acquiring new theoretical understandings that would explain how/why the algorithms work. In the case of "an AI theorem-prover that reasons similarly to how Ramanujan reasoned" this might for example require gaining a good theoretical understanding of logical uncertainty and seeing how the AI theorem-prover uses an approximate solution to logical uncertainty to guide its proof search.
It occurs to me that if the overseer understands everything that the ML model (that it's training) is doing, and the training is via some kind of local optimization algorithm like gradient descent, the overseer is essentially manually programming the ML model by gradually nudging it from some initial (e.g., random) point in configuration space. If this is a good way to think about what's happening, we could generalize the idea by letting the overseer use other ways to program the model (for example by using standard programming methodologies adapted to the model class) which can probably be much more efficient than just using the "nudging" method. This suggests that maybe IDA has less to do with ML than it first appears, or maybe that basing IDA on ML only makes sense if ML goes beyond local optimization at some point (so that the analogy with "nudging" breaks down), or we have to figure out how to do IDA safely without the overseer understanding everything that the ML model is doing (which is another another way that the analogy could break down).
It seems like for Filtered-HCH, the application in the post you linked to, you might be able to do a weaker version where you label any computation that you can't understand in kN steps as problematic, only accepting things you think you can efficiently understand. (But I don't think Paul is arguing for this weaker version).
I stumble upon interesting critical article about mathematical savants twins reported by Sacks:
http://www.pepijnvanerp.nl/articles/oliver-sackss-twins-and-prime-numbers/
Srinivasa Ramanujan is an Indian mathematician who is famously known for solving math problems with sudden and inexplicable flashes of insight. From his Wikipedia page:
and
His style of mathematical reasoning was completely novel to the mathematicians around him, and led to groundbreaking research:
If HCH is ascription universal, then it should be able to epistemically dominate an AI theorem-prover that reasons similarly to how Ramanujan reasoned. But I don't currently have any intuitions as to why explicit verbal breakdowns of reasoning should be able to replicate the intuitions that generated Ramanujan's results (or any style of reasoning employed by any mathematician since Ramanujan, for that matter).
I do think explicit verbal breakdowns of reasoning are adequate for verifying the validity of Ramanujan's results. At the very least, mathematicians since Ramanujan have been able to verify a majority of his claims.
But, as far as I'm aware, there has not been a single mathematician with Ramanujan's style of reasoning since Ramanujan himself. This makes me skeptical that explicit verbal breakdowns of reasoning would be able to replicate the intuitions that generated Ramanujan's results, which I understand (perhaps erroneously) to be a necessary prerequisite for HCH to be ascription universal.