vitriol83
vitriol83 on Hacker News
But Mochizuki didn't actually prove anything, whereas the labs have already done so.
The pessimistic scenario is the AI labs will continuously hoover up new developments in mathematics and gazump everyone in their respective fields. It's clear they have no desire to participate in any silly academic niceties, like properly assigning credit or expository work for normal humans. What incentive then do humans have to do this work ?
Generally the mood amongst research mathematicians is pretty dire, and I don't really blame them.
To be clear I think AI is super useful for mathematical research, the problem is the methods of the big labs are massively disincentivising mathematicians from engaging in research, and other associated tasks like giving seminar, teaching writing books etc. These arguably have much more value than finding an obscure counter example to Navier-Stokes.
facepalm yet pure mathematics has been instrumental in all scientific progress in modern human history including LLMs, very short sighted view
You're stating it's not a problem- but I'm giving you a reason why it is. This is serendipitously mirrored by a recent post from Terence Tao on Mastodon (
https://mathstodon.xyz/@tao/117207856734787448)
In most cases in pure mathematics, the problems are posed not because we desperately want the solution to these problems in and of themselves, but because we have seen from past experience that human-directed efforts to solve these problems tend to spur further development of the field through the efforts to solve such problems, and then to digest any partial or complete solutions that emerge for further insights. Prematurely solving the problem by purely AI-powered methods - particularly without full transparency into the solution process - can contaminate this process to the point where it actually becomes a net negative for the progress of mathematics as a whole.
yes society has let the trillion dollar company down
i find this and other efforts from anthropic somewhat antisocial. technically they have achieved their goal, but in a way which does not benefit mathematics or humanity. Kevin Buzzards headline goal was to formalise FLT, but i’m sure the real aim was to create a formalised library of mathematics which is comprehensible to humans. By solving these famous problems by brute force, they are disincentivising the important work of making it digestible for everyone else, and so in my view this work in particular has negative societal value.
majority of parents are in favour of such a ban, otherwise they wouldn't do it
if social media companies hadn't made social media a total cesspit of disinformation, child grooming and algorithmic manipulation then the outcome might have been different
mathlib and lean are currently too cumbersome for many researchers to use in say algebraic geometry, but maybe more suitable for combinatorics where it has been applied recently.
Formalised proofs and Lean in particular are still too cumbersome for the ``working'' mathematician to use it day-to-day for research-level math. But clearly there is some interest on where it may take us in future.
this seems to be the way. make great technical improvement in a way that's nothing to do with AI. the only way to make executives happy is to then tenuously link it to AI usage.
In my field which involves large legacy codebases in C++ and complex numerical algorithms implemented by PhDs. LLMs have their place but improvements in productivity are not that great because current LLMs simply make too many mistakes in this context and mistakes are usually very costly.
Everyone `in the know' appreciates this, but equally in the current environment has to play along with the AI hype machine.
It is depressing, but the true value of the current wave of LLMs in coding will become more clear over time. I think it's going to take some serious advances in architecture to make the coding assistant reliable, rather than simply scaling what we have now.
are there any tools to convert large latex documents to typst ? it looks a huge improvement, but the migration path is the only thing that's stopping me.
In places where there is not much time for code refactoring, the following is helpful:
Imagine an idealised future state of the codebase, which everyone buys into, and make sure any new feature is going in that direction.
Refactoring existing code can be death by a thousand cuts- having a parallel new codebase which is incrementally adopted can be more efficient and quicker to market.
So many times it’s necessary to ‘identify’ two more objects which are isomorphic, and the ‘canonical’ is supposed to justify why this doesn’t cause a problem.
The reason it is necessary here is that the mapping D(f) -> A_f is a priori multi valued, and we need it to be single valued.
However it’s fairly easy to make a definition which is trivially single valued , so I don’t think it’s a very instructive example of the phenomenon.
Probably more pertinent is an n-fold tensor product with different bracket ordering
This is fairly obscure but the problem he highlights can be overcome easily by localising at the saturation of S_f, for D(f)=D(g) if and only if the saturations are equal, and localising at saturation is an isomorphism
Stacks, like EGA before it, is a wonderful reference but a terrible textbook. I think even the authors would agree with this! Fortunately there are many other books from which to learn algebraic geometry, after which Stacks will start to make a lot more sense.
Modern Algebraic Geometry is indeed highly abstract, but generally the conjuring of obscure objects is with a specific goal in mind, for example
- consolidation of many types of results into a `simple' theoretical framework, I suppose this originates with Noether, and reaches it apotheosis in Bourbaki's tracts.
- embedding of 'classical' objects (solutions to polynomial equations) inside a larger 'category' (schemes) where certain mysterious relations observed in the classical world (Weil Conjectures) have a more `natural' interpretation (fixed point theorem) and light the way to a proof which would have otherwise been beyond reach
They’re all very relevant, but I try not to expect the same from OSS projects as from a VC pitch deck. After all this is work given freely.
I’m generally positive on rewriting openssl in rust, but agree the comparisons aren’t completely scientific or necessarily more important than correctness. First you should compare performance using the same implementations of cryptographic primitives as these are relatively easily fungible. We also don’t know if for example OpenSSL optimised primitives were used. Secondly the rust language only excludes memory bugs, it doesn’t exclude errors in the implementation of the tls protocol or incorrect usage of cryptographic primitives which can be just as catastrophic for security. These have been prevalent in OpenSSL and are somewhat harder to prevent a priori. For all we know these issues are worse for rustls than OpenSSL. This is where formally verified implementations would be useful.
one issue with OOP in practice that I've seen is the entanglement of the domain representation (member variables of a class) and the varied operations on that data (methods). Classic OOP encourages you to manipulate objects by methods rather than free functions, which combines potentially unrelated functionality in the same object.
my rule of thumb with objects is to keep the methods to a minimum, to the extent all classes are either interfaces, implementations of interfaces or pure data classes. obviously this approach will be natural to ML programmers.
The difficulty with learning 'modern' algebraic geometry is not only is it very dense and general, but that means the original motivation can become lost.
So I think understanding Weil conjectures are key for modern algebraic geometry. And it's always easier to understand algebraic curves (algebraic geometry with dimension 1) and their connection to Riemann surfaces (algebraic curves over the complex numbers with analytic rather then algebraic structure), as they provide motivation for many of the results and constructions.
A good introduction to Algebraic Curves and the Weil conjectures I've found is following
https://math.mit.edu/~poonen/papers/curves.pdf
For general algebraic geometry, JS Milne's notes are rather good
https://www.jmilne.org/math/CourseNotes/ag.html
and for an introduction to commutative algebra Atiyah-Macdonald's book is great.
Writing a type checker is conceptually much more specialised than just a scripting language. Certainly I have no idea how to write one!
Can anyone suggest a good embedded language with static or at least optional typing ? I feel this is a gap in the market for embedded languages.
couldn't agree more, see e.g. similar restrictions in well-known bastions of socialism singapore, denmark and australia. non-resident investment in manhattan is literally rent-seeking. perhaps if the foreign investment was redirected to regenerating post-industrial cities, or even actual job creation society as a whole would be better off
interesting article. a few more points which may be of interest
- in addition to raid it's worth having automated off-site backup. the best solution i could find is duplicity as its encrypted and supports a bunch of backends.
- freebsd supports full disk encryption using geli. with some work its possible to make it boot (only) from a usb key, so some protection if the server is stolen. I believe newer versions of Intel Atom support hardware AES acceleration, so this isn't a large overhead.
- if the memory requirements of ZFS are too large (which to be honest for a soho application they are!), then you can use UFS together with freebsd software raid1 (gmirror)
Citation needed. Plenty of people regard high-level languages as nonetheless suitable 'systems programming'. This is the first FAQ on golang.org! See also
https://ocaml.github.io/ocamlunix/
I don't think that one can necessarily equate systems programming with manual memory management (see e.g. Go). It's true that manual memory management will (probably) be more efficient and more predictable, but ultimately depends on how important that is in your application.
The article is comparing Rust principally to Python (a new dynamically typed language) and C++ (an old statically typed language). It's certainly plausible that it can bring benefits over these.
More interesting to me would be comparing it to a new-ish multi-paradigm language, of which there are many right now (e.g Swift, OCaml, Haskell, F#, Scala). It seems like in practical applications these newer FP languages will be much more productive than Rust, as memory management is much simpler. Rust's principle of zero-cost abstractions is great in theory, but can't think of many applications where it's the limiting factor except perhaps embedded devices and kernel development.
this is always a tension in writing mathematics textbooks. at one end of the extreme you have e.g. Bourbaki which are very dry, but prove a great deal very efficiently and in the utmost generality. on the other hand you have textbooks which may be not as comprehensive and will intersperse the text with illuminating examples which historically would have been the original motivation for the subject. which is best really depends on your point of view and level of sophistication in the subject. usually I try to have both types of book at hand.
what would be great is if typesetting tools improved sufficiently so that one could choose 'beginner' or 'advanced' mode when reading a maths textbook. perhaps that is too fanciful!