In his talk, The Future of Mathematics,

https://www.youtube.com/watch?v=Dp-mQ3HxgDE

 Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he justifies this as follows:

• Automation is very difficult with set theory
• Simple type theory is too simple
• Univalent type theory hasn't been successful in proof assistants

My question is about the first of these: Why is automation very difficult with set theory (compared to dependent type theory)?

In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he justifies this as follows:

• Automation is very difficult with set theory
• Simple type theory is too simple
• Univalent type theory hasn't been successful in proof assistants

My question is about the first of these: Why is automation very difficult with set theory (compared to dependent type theory)?

In his talk, The Future of Mathematics,

https://www.youtube.com/watch?v=Dp-mQ3HxgDE

Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he justifies this as follows:

• Automation is very difficult with set theory
• Simple type theory is too simple
• Univalent type theory hasn't been successful in proof assistants

My question is about the first of these: Why is automation very difficult with set theory (compared to dependent type theory)?

In his talk, The Future of Mathematics,

https://www.youtube.com/watch?v=Dp-mQ3HxgDE

Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he justifies this as follows:

• Automation is very difficult with set theory
• Simple type theory is too simple
• Univalent type theory hasn't been successful in proof assistants

My question is about the first of these: Why is automation very difficult with set theory (compared to dependent type theory)?