lambdas
Complexes are overloaded as is - cellular, simplicial, chain etc.
There was some drama when someone forked it so you could write your own JavaScript wrappers/FFI too?
In fact, these weird string terms pop up pretty often, but surely you’d want to be using de Brujin indices lest you accidentally string match two different things (can’t believe I’m saying that for an implementation of a dependently typed language).
I started to wonder how your types were glued, as I would have thought Sigma types glued along identity equivalences would give me some insight on the odd behaviour.
`reduce_comp` seemed like the place it should be. There I realised your `CTGlue` case is wrong: it seems like `partial_pairs` is in the head but dropped from the body, so they’re never glued by any equivalence.
So much has to be pragmatised, carefully considered and made concrete categories anyway that much of the category theory exists in the documentation rather in the actual code.
Resources is one. Energy, water, cost. There seems to be diminishing returns in intelligence at the moment, whilst power and memory usage continues to go up.
More “X is simply not worth our time anymore”. I can’t say with any certainty that X is on a death spiral (personally it does feel that way), but the kind of crowd who have remained in spite of Musk’s many public embarrassments (and the handling of Grok deep fakes and women) probably aren’t the kind who are passionate about the EFF
“Man, these cryptographers didn’t know a thing about tailwind. Useless!”
> Start reading books or you're going to look stupid to the people around you
Wherein the prose wasn’t at all sloppy, the tautology was certainly intentional; the implied audience of “look stupid” could be to people entirely absent of the vicinity!
You have to be very, VERY careful. With how predisposed they are to helping, they’ll turn to “dishonesty” rather than just shut down and refuse. What I tend to see is they get backed into a corner, and they’ll do something like prove something different under the guise of another:
They’ll create long pattern matching chains as to create labyrinths of state machines.
They’ll keep naming functions, values and comments to seem plausible, but you have to follow these to make sure they are what they say. A sneaky little trick is to drop important parameters in functions, they appear in the call but not in the actual body.
They’ll do something like taking a Complex value, but only working with the real projection, rounding a number, creatively making negatives not appear by abs etc etc
So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.
And when it doesn’t work, introducing an error or two in formal proof systems often means you’re getting exponentially further away from solving your problem.
I’ve not seen a convincing use that tactics or goals in the proof assistant themselves don’t already provide
A decade plus ago, you could ssh into localhost on iOS, but that got nipped in the bud with sandboxing.
I picked up Linux at 13, fortuitously just in time for the release of the Nokia 770 (later getting, and still owning the N900 too).
At that time, getting real dirty with the kernel, hardware, cross compiling etc was necessary, so 1) there were more resources 2) it was seen as mundane, busy work rather than mystical and difficult.
If I were to say how to learn the same things today, I’d probably say Gentoo is ideal - it’s insanely flexible in tinkering, has good resources on compiling the kernel and packages, and I’m a fan of crossdev for cross compiling.
Getting real dirty with hardware and electronics, the obvious answer would be one of the Raspberry Pi lineup, but if you’re very tenacious, patient and a touch unhinged, then I would actually say now’s the time to get in on RISC-V.
It’s still early days, so there’s lots of resources that have very thin abstractions between hardware <-> tooling <-> code. Devices are cheap and exciting. You’ll be on the same footing as most other people so you won’t feel like a dunce.
The cons are that a lot of RISC-V devices get shipped out with very little documentation (and sometimes only in Chinese), binary blobs making mainstream kernels difficult, and you’re learning at the same time, so you might feel you’re ice skating uphill.
Wrt to the bootloader and partition corruption; towards the twilight years of the life of the N900, when it became clear N900 had been abandoned and the N950 was still only available to select few, a bunch of smart people on the Maemo forums started reversing and writing open drivers (uboot bootloader, wifi, camera iirc), so they became pretty documented.
It was a great time - titles like Learn You A Haskell For Great Good and Land of Lisp really capture the zeitgeist.
And collecting unmanned data is still such a pain. At the moment, you stick calibration gear to a train and hope it gets as much noise free data as it can. All whilst going at least 40mph over the area you want - you’re fighting vibrations, vehicle grease, too much sunlight, not enough sunlight, rain, ballast covering things, equipment not calibrated before going out etc etc.
It picked up on the polynomial, then what it thought was a scheme/sheaf being defined is actually the finite field with six elements. It also misread “Thue” as “the”.
If you had corrected what it read from the board, then gave it the context that he was a number theorist now working for a company trying to get AI to work through proofs, then you may have got the correct answer that this appears to be them crafting problems on polynomial reduction to test how the LLM reasons about proof.
I must be an engineer for a different Network Rail
Like learning a language by strictly the grammar and having 0 vocabulary.
Same for Hartshorne’s Algebraic Geometry. Neither of these are bad textbooks at all, they both have a place on my bookshelf, but certainly better options have appeared through the years (for AG, I’d be remiss to mention Ravi Vakil’s fantastic The Rising Sea, due for a physical publishing October, and Ulrich Görtz & Torsten Wedhorn two part series)