Another example of how useful proof assistants can be for collaboration! Check this out:
https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702
This profile might be incomplete.
Open on mathstodon.xyz Talia Ringerwebsite:
Personal infoAbout:
Professor, PL/FM/SE at UIUC. Proof automation. SIGPLAN-M Founder, CCF President. They/them, ND, bi.
Wall 2 posts
Another example of how useful proof assistants can be for collaboration! Check this out: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702
Show previous comments
@TaliaRinger Hi! What happened to you is sucky, but I'm glad you found a new home and I hope they treat you well. Ooo, proof automation! ❤️ That's a follow. @TaliaRinger Ha! I had a job offer from GCHQ when I was 20, but that was 42 years ago. I don't see why that should be a problem for anyone really. Since GCHQ wouldn't tell me which area the job was in (!), I went to work for IBM instead and never looked back. (A friend accept GCHQ's offer, but hit a pretty low glass ceiling after a few years and resigned.) @TaliaRinger Oh I've seen this story before. Sorry you're dealing with this nonsense! |
(1) mei you are a legend
(2) This is exactly the kind of thing I love about proof assistants for math, how much they can open up the world of mathematics to people who wouldn't normally get to participate