pyentropy

Please. This is IAS -- the members can barely be bothered to commute.

Not a Lean expert but some of the proof tactics used to prove are probably novel? Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?

A lot of good repos (CLIs, frameworks) had 'tree' unicode directory structure with like ├──, └──, and │ , as well as emojis for passing/failed tests and README docs maybe a unicode arrow or two, but LLMs absolutely overuse it.

I don't know why chatbots prefer → over -> so much. It's becoming a countersignal compared to the old terminal customization era, where arrow ligatures were a signal of effort.

Vedran Miletić doesn't sound German to me! :-)

In times when software eng teams push for maximizing token usage, Tao's public view is to encourage verification, limit AI use for tasks that have real-life consequences and prevent low-effort papers that exhaust the review pipeline?

He also focuses on training the next generation of mathematicians and prioritizing the process of slow digestion of results, which to me sounds very.. reasonable?

Note that the SAIR lecture is from 6 months ago, this Beamer presentation is from 2 days ago.

I'm considering the possibility that it's good to break the prefix and cache because the LLM itself was rewarded (during post-training) with different prefixes/system prompts, each containing reasoning traces of the correct size.

I might be very very wrong though and LLMs disagree with me, insisting that cache is preserved and the system message doesn't have to change (even though it often contains effort level in context) if effort level changes across turns, and that all you have to do is tell the inference lib that parses think tags to early-close think tags that are too long.