戻る

> Once the systems are this mature,

コンピュータツールが進歩して紙の上で論ずるのと同じくらい簡単にコンピュータ上で定理証明をできるようになれば、

> it might be the case that future generations of mathematicians will not have to worry about what people like Grothendieck mean by equality,

将来の数学者はグロタンディークのような人々が equality というとき何を意味していたのかに煩わされる (have to worry about) ことはなくなるかもしれない、

> because the systems will allow us to use the concept the way that it is currently used by mathematicians in practice.

ツールによって、数学者が現状やっているように (曖昧に) この概念も使えるようになっているだろうから。