A self-study Math genius Vladimir Voevodsky, Fields Medalist, Russian.

Voevodsky borrowed idea from Computer Science (“Interface” =hide implementation details) to Math, and vice-versa, from Math to Computer Science :

Homotopy Type Theory (HoTT)

**Result**: Computer to prove math theorems.

**Computer Science** Idea:

- Hiding Implementation Detail
- Black Box “Interface”
**Type (类)**: Boolean, Integer, String, … (stronger structure than ＂Set＂ 集合)

**Math** Idea (Abstract Geometry : Algebraic Geometry) :

**Homotopy**(**同伦**)- eg. Cup ~ Donut, both are
**homotopic**or same “**Type**” (in Computer) **Isomorphism**is**Equality “=”****Homotopy Type Theory**(**HoTT):**: both objects are considered “=” if they are__Univalent Theorem__*isomorphic*(prove if 1-to-1 correspondence 对应)