Remix.run Logo
▲ fspeech 21 hours ago

I actually believe that this isn't the way to go when proof is cheap. Due to the straitjackets of type theory sharing proofs across domains is painful for most human readers to consume. With AI it's much easier to specialize theories. It's just not worth the cognitive cost to build on top of broad and shallow theories. To have any hope in keeping up with AI we need to instead better appeal to the largest component of our brain - namely our visual cortex.

▲eru 18 hours ago | parent | next [-]

The visual cortex is not the largest component of our brain.

▲Ericson2314 18 hours ago | parent | prev [-]

Uh by "specialized theories" you mean less general results. Such a straightjacket is totally against the spirit of math.

▲fspeech 15 hours ago | parent [-]

Have you looked at how much Lean proofs are just translations between types?