A new generation has arrived. The other day a freshmen showed me 10k lines of code in a single file, written by him and an LLM in a week. It uses machine learning to find small boolean formulas that match a given truth table. A freshman. 10000 lines of code in main.py. It works. Oh yeah, and some of them think Lean 4 is common knowledge.

0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/andrejbauer/statuses/115586453363278378 on your instance and quote it. (Note that quoting is not supported in Mastodon.)