But he's also using AI for formally verified math and for ideas in solving math problems. The part about it being ok because it is a supplement just means ok that these aren't formally verified and may have bugs, and may also mean ok to not credit the AI for the paper as it is just a visual supplement and not the main work.