HN user
There was recently an announcement that a group trying to formalize it found a gap exactly where other mathematicians were pointing. So to the extent there was any doubt, it should be gone now--the proof was incorrect.
But I agree LLMs have a lot of potential for checking proofs--both informally (they can read quickly and find gaps) and formally (by attempting to formalize).
I believe that "single source of truth" is a principle that should always be followed. If there's duplicated code where it'd be a bug if they diverge, then you should refactor. It creates a long-distance coupling in your code that may be invisible to future developers until a bug emerges.
But with that in mind, I mostly agree with the article: if it's not a violation of "single source of truth", then abstractions are just a convenience. If it starts being inconvenient, then it's not doing its job and there's no reason to use it. It's a serious code smell if a function needs several flags for custom behavior; that means it's probably the wrong abstraction or violating the single responsibility principle. If there is a legit need for lots of customization, an often-good way to handle is to take a function/functor as an argument for the customization. E.g., rather than `solve(f:double -> double, max_iters = 99, x_abs_tol = 1e-15, x_rel_tol = 1e-15, ...)` you can do `solve(f:double -> double, stopping_criteria: StoppingCriteriaClass)`
One of the authors said in a reddit comment (and I hope I am summarizing accurately) that it's impossible to show a diagram as the smallest instance of the technique gives like 10^1000000 points.
The problem was pretty well known, and had many human attempts. There's some room to argue that the right humans hadn't attempted it, as the solution used advanced methods from another field of math. But imho, whereas many prior AI victories could be explained by not enough human attention, there is no such excuse in this case, and one should acknowledge this is a notable achievement.
This is happening to other forms of competitive programming too. The most recent AIs have problem solving skills rivaling top humans, and so if AI can't be easily banned, the competition is dominated by AI agents.
I thought code golf would take longer for AIs because there's so little training data (it's more niche), but we're seeing AIs starting to match expert humans there too. Sucks because golf has been my favorite type of programming puzzle.
It's crazy how far AIs have come in problem solving ability.
You can't do this for general functions, but it's fine to do in cases where the definition of f naturally embeds into the rationals. For example, a polynomial over Z is also a polynomial over Q or C.
The movement from R to C can be done rigorously. It gets hand-waved away in more application-oriented math courses, but it's done properly in higher level theoretically-focused courses. Lifting from a smaller field (or other algebraic structure) to a larger one is a very powerful idea because it often reveals more structure that is not visible in the smaller field. Some good examples are using complex eigenvalues to understand real matrices, or using complex analysis to evaluate integrals over R.
You can go farther and say that you can't even construct real numbers without strong enough axioms. Theories of first order arithmetic, like Peano arithmetic, can talk about computable reals but not reals in general.