jaykru

I think the concern is that it could be seen as minimizing the harm done to those affected, but I personally think this is kind of a hypersensitive overcorrection :P

Would you rather ancient issues to which our bodies have apparently adapted or new issues we haven't yet had time to adapt to? I'm not sure on the answer myself but it doesn't appear as clear cut as no worms => no issues.

To boot even if you skip the free models, you could probably do a year's DIY assistance with 50 cents worth of GLM or Deepseek tokens. And the really costly jobs are ones where an AI assistant won't really help since, shockingly, most of the cost is hours of labor which you would have to do yourself.

That's super interesting. I wonder if you've tried optimizing for type-checking duration of a richly dependently typed program and gotten viscerally nicer code out of that.

Curry-Howard doesn't buy you any shortcuts to capability. Surely no expense has been spared in training models to write good (well modularized, robust, generic etc.) code, and yet they still write slop (poorly structured, overfit to specification gaps, etc.) We see the same sloppish habits in their mathematics, perhaps transported along the CH iso. So "train[ing] agents to write better proofs" seems to me like a grand challenge problem for AI research, just like getting them to write good code. It won't be solved just by noticing that the two problems are isomorphic: we'll keep getting models that are a little better at grinding out proofs, hence a little better at grinding out programs, but the abstraction wall won't magically drop in either world just because the same limited behaviors can be transported along CH.

the autoformalization could be proving a subtly distinct result; if the area is not in mathlib already there's likely not a good reference theorem specification to use for a comparator check. or it could be exploiting kernel bugs. just using a second checker kernel is not enough; there has been an example of a model interpolating bugs across multiple checkers in a single bogus proof.

I kind of feel motte-and-bailey'd here. You began by questioning the value of human understanding in mathematics and I've explained (exactly as you've said) why it is currently on the critical path of outcomes in science and engineering with value to humanity almost nobody would dispute. This new question, where human understanding of mathematics isn't on the critical path of anything, is something I can't argue, in the same way that I can't argue for the intrinsic value or meaning of essentially any human activity without resorting to what amount to basically religious axioms.

this is the term of art in the mathematics community. considering that the vast majority of the results don't come with a typechecking lean formalization, i don't think it's off base at all either.

many of these are not accompanied with leanslop

The fact that you need to ask "the right questions" is why it's not AGI. A general intelligence should be able to ask of its own volition the interesting questions required to advance its goals.