 |
Post AvqeDwBNNvsR6WHf7o by [email protected] |
 |
More posts by [email protected] |
|
Post #AvqeDvcHUPnvLfrdQG by [email protected] |
|
0 likes, 0 repeats |
|
|
|
"In the end, the Party would announce that two and two made five, and you … |
|
|
|
Post #AvqeDvk51Q2hjrVrZw by [email protected] |
|
0 likes, 0 repeats |
|
|
|
In modern mathematics we take it for granted that there is a consensus standard… |
|
|
|
Post #AvqeDvrAb3iK5qpWd6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
This ability to arrive at consensus by recognizing an objective standard of tru… |
|
|
|
Post #AvqeDvxYDKomPdocZk by [email protected] |
|
0 likes, 0 repeats |
|
|
|
And even in mathematics, our consensus standard (which was painfully acquired o… |
|
|
|
Post #AvqeDw3ZqvdeiKdQy8 by [email protected] |
|
0 likes, 1 repeats |
|
|
|
More recently, we face the real and disturbing possibility that certain directi… |
|
|
|
Post #AvqeDwBNNvsR6WHf7o by [email protected] |
|
0 likes, 1 repeats |
|
|
|
@tao ... relentlessly critized for even the slightest typo or ...s/critized/cri… |
|
|
|
Post #AvqeDwN4gREbgnl0MK by [email protected] |
|
0 likes, 1 repeats |
|
|
|
One potential bulwark against such politicization of mathematical truth is the … |
|
|
|
Post #AvqxqxYi6FaBnOWEm8 by [email protected] |
|
0 likes, 1 repeats |
|
|
|
@tao I feel like in non-mathematical sciences, it's far too easy to produce… |
|
|
|
Post #AwEtFZ3MVmtJ3Uo7e4 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao Cf. https://xkcd.com/263/"a(b+c)=(ab)+(ac). Politicize that, bitches… |
|
|
|
Post #AwEtI5zuzoQHoHP5Zg by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao the fact that lean specifically is completely governed by Microsoft, which… |
|
|
|
Post #AwEtI66ealoK9AYT4a by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@fanf42 While it is true that Lean was originally developed by researchers at M… |
|
|
|
Post #AwEtI6CgEMdCRrNHSy by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao oh nice, I missed the move towards an fro! Do you have a link towards the … |
|
|
|
Post #AwEtI6ILtHAUjS1oJ6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@fanf42 The various subpages of https://lean-lang.org/fro contain some relevant… |
|
|
|
Post #AwEtI6P5UEYX4LBBo0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao thank you son much! 👍 |
|
|
|
Post #AwEtICQ17grfixf15U by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao Metamath is not math. It’s meta-consensus—an infinite game of symbol p… |
|
|
|
Post #AwEtICXoeh6S79JFFA by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao Tao retells math history as a march toward objective truth—but that’s … |
|
|
|
Post #AwEtICgK93uOXXI2VM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@[email protected] @tao Tao’s worry isn’t about truth—it’s about contr… |
|
|
|
Post #AwEtIDutYN9sN17Br6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@[email protected] @tao The infinite universe hierarchy introduces metaphysica… |
|
|
|
Post #AwEtJemT9uIhyerDZw by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao one of the craziest thing I learned when I got into college and start read… |
|
|
|
Post #AwEtOndHfvUusY0t3A by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@oec Ha! Now fixed. |
|
|
|
Post #AwEtQFsI9oykl9j8wC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@mdcory @[email protected] @tao mate did you just post an output of chatgpt pr… |
|
|
|
Post #AwEtQFz1kmMn62sWR6 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@extenebris @[email protected] @tao What? No. Actually, I edited the post beca… |
|
|
|
Post #AwEtRUcKpWy0lxqzFw by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@shironeko @tao Sometimes you're better off NOT seeing the code. |
|
|
|
Post #AwEtRUi0URVJ3YVW64 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bks @tao for them I guess, lol |
|
|
|
Post #AwEtb94LnghKq1Ynwm by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao is math whatever lean tells it is? |
|
|
|
Post #AwEtbM0Zh2Oyy4tTMm by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao I can see where this is coming from, but ultimately, the hope for mechanis… |
|
|
|
Post #AwEtehfrb1QP24nrxg by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@tao I think the more common exploit of ostensibly formally verified claims wil… |
|
|
|
Post #AwEtfbzIDyEzgYKB1M by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@mdcory @tao woa, who would've thought that my comment would result in pett… |
|
|
|
Post #AwEtfc4xssmHy8yhrU by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@extenebris @tao Your comment was ad hominem—get it? You're a suppositiou… |
|
|
|
Post #AwEtfcBhTqAKJ285MO by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@extenebris @tao Please tell me more about your views of type theory in Lean. I… |
|
|
|
Post #AwEttrLptpw7OAf9FY by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@acowley @tao Personally I call this mismatch this "the pitfall of interpr… |
