Im not opposed to the use of proof assistant software for difficult theorems. An... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		chobytes on April 29, 2021 \| parent \| context \| favorite \| on: Category theory is a universal modeling language Im not opposed to the use of proof assistant software for difficult theorems. And if one foundation or another is more applicable to that software, then thats fine. Its more the narrative of the grand unification of mathematics thats spun around 'foundational theories' that irks me. In reality its just various emulation schemes. Rephrasing other mathematicians work and claiming fundamental status, while not producing many novel theorems... just strikes me as very distasteful.

jkhdigital on April 30, 2021 [–]

Only if one allows their ego to get in the way of the search for abstract truth does this become “distasteful”.

There’s no claim of fundamental status here, merely a desire to standardize aspects of what is very much an artisanal process.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact