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.
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
It seems though that we would want the computer to be able to do this kind of reasoning itself, and not rely on humans "pre-resolving" all such problems.
I understood the presentation to be on the distinction between equality and isomorphism and when an isomorphism "is an equality". From the slide on homotopy type theory I get the impression that he finds it unsatisfactory to simply consider all isomorphisms as equalities.
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
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.
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
reply