roystgnr
16hr ago
Manhattan. For the "adventurous" version, I like to use both rye and bourbon, add a dash of Angostura bitters, a dash of Cherry Heering, shake with ice and strain into a martini glass with a maraschino cherry or two skewered for a garnish, but the simplest "2 oz any whiskey, 1 oz sweet vermouth, over ice" is already pretty good.
If you like whiskey sours and you make your own sour mix, try reducing the sugar a bit and adding amaretto. Amaretto sours are too weak and too sweet, but if you usee whiskey to fix the one problem and tweak the mix to fix the other then it's a great flavor.
Most results produced with an honest human who understands what they're doing will be fine. There were a few corner-case bugs in Lean itself discovered recently, and those might not be the last, but they'll at least be rare. And although you can slip in an "just assume X" to get you to your proof of Y, meaning it's then really a proof of X⇒Y, anyone who really understands the problem will understand that "see what you can prove assuming X" is an intermediate step to proving Y, not the final result.
I still have to say "most" here, because the trouble with a proof written in Lean is that it is written in Lean. If you're working on the frontiers of mathematics then you're almost certainly going to have to formalize your own definitions, and a mistake in formalizing a definition is not a mistake a formal system can detect. A verifier will simply verify that you did indeed prove the precise thing you told it you were proving, even if that thing is not precisely the thing that you were writing in English about proving.
But the big catch here is "honest human who understands what they're doing". There will be people who add new axioms (or who are happy when their LLM adds new axioms) "because that made it run" without realizing that's what they've done. There will be jerks or cranks who do this deliberately. IIRC there was a guy on
TwitterX a month or two ago ranting about his wonderful new major proof, all formalized in Lean and everything, who apparently didn't pay attention when his use of thesorryplaceholder triggered its warnings. And at the frontiers of mathematics, the honest human who understands what they're doing may end up vastly outnumbered by jerks and cranks after the latter feel "empowered" by AI. Even before LLMs there were relatively low-level bits of mathematics famous for breaking amateurs' minds and turning them into cranks. I assume we'll stave off most of them by getting into the habit of checking new Lean code for "hacks" rather than pure technical validity, and that'll work for any proof regarding stuff that's already defined in mathlib, but it still won't stop the cranks altogether.More options
Context Copy link