Double-checking, is this more like the recent DFT improvement where even the word-RAM model of computation doesn't justify the fraction of a log factor they eliminated because of an assumption of arbitrary-precision arithmetic, or has ETH actually fallen with the Lean proof being formulated appropriately? Do we know yet?
The DFT result isn't RAM specific. It holds up in multi-tape turing machines. (it is, however, galactic).
loading story #50254889
loading story #50255160