There are proof assistants https://en.wikipedia.org/wiki/Proof_assistant that would encode a mathematical proof as code, and verify its correctness for you.

Writing completely formal proof is very painstaking, because it means we will need to flash out a lot and a lot of details (which are mostly trivial for experts) for computers to accept it, and we also need to know how to work with proof assistants.

Human proofs often ignore these details to make it readable, yet also make it more prone to mistakes. Whereas formalized prove in proof assistant can very rarely be wrong (unless there is an unlikely bug in the assistant kernel), but mostly unreadable (unless the proof is incredibly elegant).

So in general, translating good human proof to computer proof requires more expert labor than huge conceptual innovation, yet it usually require the steep learning curve of understanding the ins and outs of a proof assistant, which can take years of experience.

LLM used to be pretty bad at this because even filling in trivial details can quickly derail them. Recently a few flagship coding model are finally able to do this, albeit with a large amount of token consumption in thinking.

My businesses don't depend on Anthropic, so that doesn't worry me at all - I'm using Claude code as my daily driver when I'm building software just because after trying a bunch of options it has consistently made me more productive than anything else over the last 9 months. Every month or so I try the latest open weight models which I can run locally, when they get good enough for me to have an acceptable productive dev experience fully offline locally I'll be very happy. Gemma 4 is already a major step forwards there and I've used it for some small local hobby projects, but I still get much more done when I'm working on large complex code projects if I use Claude code. If they removed their $200/month subscription and stopped subsidizing compute, I'd likely switch to another tool/chase whoever else is burning VC money for a bit, while accelerating my adoption of local models, accepting lower productivity.

Nah, I'm just moving with the times in an industry which didn't give me much choice - was laid off twice and the contract roles I ended up managing to get were companies who were already heavily using and expecting usage of AI. Tbh though I see it like the early days of the internet - and while I'm not a fan of big tech, wish the US was less corrupt and wish capitalism wasn't so rampant, at this point IMO the cat is very much out of the bag and the industry has moved on - at least where I am right now. I'd imagine if I move back to Britain the usage/attitudes towards AI are probably pretty different

Well realistically my favourite product is my most recent passion project, which is my karaoke generator platform https://nomadkaraoke.com/

It makes people happy every day, and I get the superpower of being able to let guests at my weekly karaoke night sing literally anything they want (cos I can generate it on the night so they can sing a good quality karaoke version of it even if it's a super niche song)

I don't think that's a question 😅 I work on my garden at the weekends and cycle a bunch thanks - I don't have (or want) kids so I have a bit more free energy to build stuff without sacrificing my work/life balance too much compared to most folks my age