[HN Gopher] The Math Is Haunted
       ___________________________________________________________________
        
       The Math Is Haunted
        
       Author : danabramov
       Score  : 61 points
       Date   : 2025-07-30 20:46 UTC (2 hours ago)
        
 (HTM) web link (overreacted.io)
 (TXT) w3m dump (overreacted.io)
        
       | 7373737373 wrote:
       | One problem I have with learning Lean is that tactics - like rfl
       | in the example - are overloaded, and their full semantics not
       | completely explained/understandable from the tutorials. Unlike,
       | say, C programming where one may understand what happens to the
       | program state down to the bit, it feels too fuzzy. And the
       | rewrite (rw) tactic syntax doesn't feel natural either.
        
         | danabramov wrote:
         | Yeah the documentation is also quite fragmented because tactics
         | are user-definable and some are from Lean vs from Mathlib etc.
         | I've gotten quite decent at using the basic ones but I still
         | sometimes ask on Zulip if something isn't working as I
         | expected.
        
         | LegionMammal978 wrote:
         | Yeah, I've similarly found the tactics in Coq (now Rocq)
         | difficult to internalize. E.g., I might have "A = B" and
         | "P(A,A)" available, and I want to conclude "P(A,B)", but the
         | rewrite will fail for some arcane reason. (Issues with the
         | definition of some of the intermediate structures, I'd
         | imagine.)
         | 
         | On the other end of the spectrum, I've recently been playing
         | with Metamath and its set.mm database, which has no
         | programmable tactics at all, only concrete inferences that can
         | be used in a proof. (E.g., the modus ponens inference ax-mp
         | says that "|- ph" and "|- ( ph -> ps )" prove "|- ps", where
         | "ph" and "ps" are variables that can be substituted.) Alas,
         | it's not much better, since now you have to memorize all the
         | utility lemmas you might need!
        
           | 7373737373 wrote:
           | Agreed - the Metamath base language (and its verifier) seem
           | to be the most tractable of all I've seen, although it is
           | probably still quite far away from the complexity of the high
           | level language(s) that compile to it.
           | 
           | Derived from it, the currently best attempt to achieve an
           | unambiguous and secure language seems to be Metamath Zero:
           | https://github.com/digama0/mm0
        
       | kevinqi wrote:
       | as someone who hasn't seen Lean before but was curious from
       | alphaproof, love the intro! curious if you can mention what
       | you're working on in Lean?
        
         | danabramov wrote:
         | For now I'm just learning math with it!
         | 
         | Currently I'm going through https://github.com/teorth/analysis
         | (Tao's Lean companion to his textbook) and filling in the
         | `sorry`s in the exercises (my solutions are in
         | https://github.com/gaearon/analysis-solutions).
        
           | kevinqi wrote:
           | very cool. btw, I also love that "sorry" is the "any"
           | equivalent in Lean
        
       | 7373737373 wrote:
       | Does Lean have some sort of verification mode for untrusted
       | proofs that guarantees that a given proof certainly does not use
       | any "sorry" (however indirectly), and does not add to the
       | "proving power" of some separately given fixed set of axioms with
       | further axioms or definitions?
        
         | jonny_eh wrote:
         | Apparently this is possible with macros? I dunno:
         | https://github.com/leanprover/lean3/issues/1355
        
         | masterjack wrote:
         | Yes, you can `print axioms` to make sure no axioms were added,
         | make sure it compiles with no warnings or errors. There's also
         | a SafeVerify utility that checks more thoroughly and catches
         | some tricks that RL systems have found
        
         | danabramov wrote:
         | Does `#print axioms some_theorem` mentioned at the end of the
         | article qualify? This would show if it depends on `sorry`, even
         | transitively, or on some axioms you haven't vetted.
        
           | 7373737373 wrote:
           | Oh, I missed that, thanks! It would be cool to use this to
           | visualize the current state and progress on, and depth of the
           | "proof dependency graph"!
        
       | cubefox wrote:
       | One thing I didn't know until recently was that Lean doesn't
       | solve the problem of verifying that a formal theorem actually
       | states what it is supposed to state rather than something else.
       | 
       | In some cases that's not an issue, because the formal statement
       | of the theorem is very simple. E.g. for Fermat's Last Theorem,
       | which can be formally expressed with "(x y z : N+) (n : N) (hn :
       | n > 2) : x^n + y^n [?] z^n". But in other cases it might be much
       | harder to verify that a formal statement actually matches the
       | intuitive informal statement we want.
       | 
       | Of course, Lean or similar languages still offer the huge
       | potential of verifying that a formal statement is provable, even
       | if they don't help with verifying that the formal statement
       | matches the intended informal statement in natural language.
        
       ___________________________________________________________________
       (page generated 2025-07-30 23:00 UTC)