logoalt Hacker News

ModernMechtoday at 1:36 PM1 replyview on HN

So was Lean. Did Lean solve it?


Replies

zamadatixtoday at 2:00 PM

Nothing is solved in isolation but credit usually goes to wherever the new work in the paper comes from instead of the whole mountain of previous mathematics or existing tools used. The most relevant of those get referenced and then this reference tree builds a tree of collective base work needed across history.

show 1 reply