Terence Tao, "Machine Assisted Proof" [video]

I was trying to convince people that GPT4 was super helpful for learning programming langauges. For getting over the hump between knowing the basics and actually being familar at building things in the language and I used Tao as an example.

Tao is finding ChatGPT helpful for proofs, as a sort of brainstorm partner. And if it works for him, then why can't it work for me trying to cross the intermediate gap in learning Rust?

These tools work best when you know what you are doing, know the questions to ask, but are in unfamilar territory.