As someone who is currently getting a PhD in mathematics I wish I could use Lean. The main problem for me is that the area I work in hasn't been formalized in Lean yet. I tried for like a week, but didn't get very far... I only managed to implement the definition of Poisson point process (kinda). I concluded that it wasn't worth spending my time to create this feedback loop and I'd rather work based on vibes.
I am jealous of the next generation of mathematicians that are forced to write down everything using formal verification. They will be better than the current generation.
Most people disagreed with the following two statements: "I think the probability of AGI before 2030 is above 50%" and "AI-to-human safety is fundamentally the same kind of problem as any interspecies animal-to-animal cooperation problem".
Most people agreed with the statements: "Brain-computer interfaces (e.g. neuralink tech) that is strong and safe enough to be disruptive will not be developed before AGI." and "Corporate or academic labs are likely to build AGI before any state actor does."
There seems to be two large groups who's main disagreement is about the statement " I think the probability of AGI before 2040 is above 50%". We will call people agreeing Group A and people disagreeing Group B.
Group A agreed with "By 2035 it will be possible to train and run an AGI on fewer compute resources than required by PaLM today (if society survives that long)." and "I think establishing a norm of safety testing new SotA models in secure sandboxes is a near-term priority."
Group B agreed with "I think the chance of an AI takeover is less than 15%".
The most uncertainty was around the following two statements: "The 'Long Reflection' seems like a good idea, and I hope humanity manages to achieve that state." and "TurnTrout's 'training story' about a diamond-maximizer seemed fatally flawed, prone to catastrophic failure."
As someone who is currently getting a PhD in mathematics I wish I could use Lean. The main problem for me is that the area I work in hasn't been formalized in Lean yet. I tried for like a week, but didn't get very far... I only managed to implement the definition of Poisson point process (kinda). I concluded that it wasn't worth spending my time to create this feedback loop and I'd rather work based on vibes.
I am jealous of the next generation of mathematicians that are forced to write down everything using formal verification. They will be better than the current generation.