HNHacker News
TopNewBestAskShowJobs

ocfnash

1,664 karma · joined January 12, 2014

http://olivernash.org
submissionscomments
ocfnash··on Remembering Magnetic Memories and the Apollo AGC
According to http://madrona.ca/e/coremem/index.html

> I have seen it [core memory] in service as recently as 2004 in a telephony control application

ocfnash··on Growing up in “404 Not Found”: China's nuclear city in the Gobi Desert
Thank you for sharing these memories.

I'd be very interested to hear any thoughts you might have about Jung Chang's book "Wild Swans".

I read this book a year or two ago and learned a lot from it, but I also learned that many people who grew up in China take issue with the author's account. I'd be grateful for any remarks you may be able to share.

ocfnash··on Ask HN: Who is hiring? (September 2025)
Mathlib Initiative | DevOps Engineer | Fully-remote | Full-time

The Mathlib Initiative is a new programme of Renaissance Philanthropy. We exist to support Lean's open-source library of formal mathematics known as Mathlib https://leanprover-community.github.io/

Please apply directly at: https://www.renaissancephilanthropy.org/careers/devops-engin...

ocfnash··on One universal antiviral to rule them all?
Most viruses are bacteriophages, so I imagine bacteria would run wild!
ocfnash··on OpenAI claiming gold medal standard at IMO 2025
According to the 6/N from this series, they are claiming full marks for problems 1 -- 5

https://x.com/alexwei_/status/1946477742855532918

ocfnash··on YouTube's new anti-adblock measures
I'm a bit surprised nobody seems to have mentioned http://fixyt.com

I have a bookmarklet:

javascript:(function() {window.location=window.location.toString().replace(/^https:\/\/www.youtube\./,'http://fixyt.');})()

and whenever I want to watch a YouTube video, I just click that and enjoy an ad-free experience.

ocfnash··on The Dome (2005)
I think it is worth comparing this problem with the question of the behaviour of a particle placed at the apex of a cone. I claim it is clear that in this case, the problem is clearly not well-posed because the apex is a singular point: the slope at the apex is undefined. The singular nature of the slope (first derivative) is the issue.

This "dome" is essentially the same issue just with the singularity buried one level deeper: you need to take second derivatives to see it. Indeed a planar cross section containing the vertical axis through its center is a graph of the equation $y^2 = |x|^3$ (up to constants) and this is not twice differentiable at $x = y = 0$. Newtonian mechanics is governed by a second order differential equation, so we need a C^2 regularity assumption to get uniqueness.

So for me there is not really any more philosophically interesting than the question about a particle balancing at the apex of a cone.

ocfnash··on Ask HN: What is the best thing you read in 2024?
If you like these, you should try the Uncle Fred books. Of course almost everything by Wodehouse is a sublime masterpiece.
ocfnash··on The electrostatic world of insects
As a kid, the alliterative mnemonic we were taught was "current kills".
ocfnash··on AI solves International Math Olympiad problems at silver medal level
The computer did find the answers itself. I.e., it found "even integers" for P1, "{1,1}" for P2, and "2" for P6. It then also provided provided a Lean proof in each case.
ocfnash··on Terence Tao on proof checkers and AI programs
If you are curious, I encourage you to look up The Sphere Eversion Project [1].

It was a project in which we formalised a version of Gromov's (open, ample) h-principle for first order differential relations. Part of the reason it was carried out was to demonstrate what is involved formalising something in differential topology.

1. https://leanprover-community.github.io/sphere-eversion/

ocfnash··on The Quintic, the Icosahedron, and Elliptic Curves [pdf]
You can see Klein's work in action in Python here if you're interested:

https://github.com/ocfnash/icosahedral_quintic

ocfnash··on Lean4 helped Terence Tao discover a small bug in his recent paper
You can even follow his progress on GitHub here:

https://github.com/teorth/symmetric_project/

ocfnash··on Solving a simple puzzle using SymPy
Note that this argument does not depend on the fact that the blue rectangle also has equal area.

This argument thus teaches us even more, namely: the configuration of the four equal-area rectangles orange, yellow, green, pink has the special property that if you widen it to get a square, the extra piece you add also has equal area.

ocfnash··on Nintendo filed numerous patents for Zelda: Tears of the Kingdom mechanics
I salute your intention to find the silver lining but my experience reading patents is that they are hard to read. I believe this is because their job is not to convey information but rather to fulfill a legal requirement. I also believe that less restriction of these "inventions" would lead to a greater proliferation of truly useful explanations. No doubt there are exceptions but this has been my experience.
ocfnash··on YouTube is testing a more aggressive approach against ad blockers
I've been using fixyt.com to avoid YouTube grossness for years. Thanks to the bookmarklet below, whenever I land at youtube.com I'm only ever a click away from escaping their awful, awful app.

javascript:(function() {window.location=window.location.toString().replace(/^https:\/\/www.youtube\./,'http://fixyt.');})()

ocfnash··on Vincent van Gogh's paintings and drawings
A couple of years ago I read Irving Stone's biography of Van Gogh [1] and it very much enriched my experience of Van Gogh's art.

The book is based largely on a collection of letters between Vincent and his brother Theo and is quite moving sometimes.

I recommend it!

[1] https://en.wikipedia.org/wiki/Lust_for_Life_(novel)

ocfnash··on Discovering that a Bluetooth car battery monitor is siphoning location data
Presumably one could now punish this behaviour by spamming the API with a firehose of fake data?
ocfnash··on Ireland’s DPC set to hit Meta with record privacy fine over US data transfers
I note that this also appeared just days ago: https://www.irishtimes.com/business/2023/05/15/three-quarter...

I'm not quite sure what conclusions to draw.

ocfnash··on Dancing Plague of 1518
The date of the last person executed by guillotine in France is surprisingly recent.
ocfnash··on Scratch is the world’s largest coding community for children
I mentioned this in a reply to a comment below but I think it is worth repeating at top level: there is a great app called Pytch which is a bridge between Scratch and Python (and runs in a web browser).

I always recommend it to anyone teaching young kids to program.

You can find it here: https://www.pytch.org/app/

ocfnash··on Scratch is the world’s largest coding community for children
There is a marvelous app designed to solve exactly this problem called Pytch: https://www.pytch.org/app/
ocfnash··on Less than half of California students read or do math at grade level
It's not especially relevant but I can't help being reminded of VerizonMath https://www.youtube.com/watch?v=MShv_74FNWU
ocfnash··on Ramanujan Factorial Approximation (2012)
Weirdly, I was just sent this same blog post a few days ago. I guess it’s doing the rounds. I’ll repeat what I said to my friend who sent it.

Ramanujan was of course an extremely talented mathematician but IMHO, there is an unnecessary cult of mystery about him. In particular, there is no mystery as to where this formula comes from: it is obtained from applying a standard technique to a standard formula. Also, it is just one instance, I’ll call it the “k = 6” instance, of a family of such formulae and I’m near-certain the “k = 2” case was known before Ramanujan (on phone or would double check).

In any case, the standard formula is just the series expansion for: n! / sqrt{2πn} (n/e)^n and the standard technique is to raise both sides of a series expansion to some power, k say, multiply out one side, and then take k-th roots again.

In this case we just need to calculate: (1 + 1/12n + 1/288n^2 - 139/51840n^3 + O(1/n^4))^6 = 1 + 1/2n + 1/8n^2 + 1/240n^3 + O(1/n^4)

After taking the 6th root again we multiply inside by 8n^3 (from the LHS) and you get Ramanujan’s formula.

ocfnash··on Understanding Jane Street
Assuming it is accurate, the final sentence in this article is especially notable.
ocfnash··on Ryanair Condemns Hungarian Govt’s Idiotic ‘Excess Profits’ Tax
I expect that the comment above was referring to the negative externalities, not captured by the financial side.

For example, having more free time is probably not adequate compensation for the greenhouse gases emitted (at the societal level at least).

ocfnash··on Réunion: the postmen of the peaks
You lucky thing! My wife and I visited Réunion in 2019 and absolutely loved it.

One thing that struck us was just how much it felt like what it is: a piece of France in the tropics. We had just come from Mauritius which felt quite remote but arriving in Réunion suddenly felt like we were back in Europe.

ocfnash··on Réunion: the postmen of the peaks
I interpret this as a simple thinko, not unlike the expression "I could care less". As Al Yankovic says:

'Like "I could care less", That means you do care, At least a little'

ocfnash··on Reverse engineering a mysterious UDP stream in my hotel (2016)
I think it's unlikely the lights happened to send the right IR pattern.

I once hooked a TV remote up to a logic analyser to have a look and here's how the on/off signal looked for this brand: http://olivernash.org/2010/01/03/the-telly-terminator/rc6-6-...

Some further details here: http://olivernash.org/2010/01/03/the-telly-terminator/

Of course it's still possible!

ocfnash··on A mathematical formalisation challenge by Peter Scholze
The Lean Community website [1] is a great place to start. Depending on your background you might like to dive right into the Natural Number Game [2] or the Theorem Proving in Lean [3] (both linked from the Community site).

1. https://leanprover-community.github.io/

2. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game...

3. https://leanprover.github.io/theorem_proving_in_lean/

Page 1 of 6Next →