logoalt Hacker News

ted_dunning • today at 4:41 PM • 1 reply • view on HN

This is the common experience in replicating a published paper by hand ... it is common to find "obvious" aspects that are anything but.

The scary thing is when AIs generate unreadable formal proofs and then effectively lie (or fabulate, to be polite-ish) about the natural language version of the steps. Since the natural language version is arguably the most important aspect of a solution to a flagship problem, this fabulation deflates the value of the solution while the existence of the solution discourages further work on the problem.

Replies

ndriscoll • today at 5:06 PM

I have hopes that this is primarily a matter of needing more engineering work on ergonomic formal languages and better building a language that "looks like math." e.g. when doing linear algebra stuff, a linear combination might be defined as a finitely supported function from an index set to your space, which is fine, but ugly and maybe conceptually overwhelming on first meeting, so I did some toying with little macros and eventually a small python Lean -> HTML renderer to do some basic transformations to make it look more like typical math notation with like \Sigma_{i \in I} a_i, or with a_0+...+a_n, etc. (to... not fantastic success, but I think there's still something to the idea).

I think a lot of math notation isn't wrong given a context, so in theory we should be able to translate it into something formal. Maybe also generate living documents where you can e.g. write `h : some_claim := by details(by rw[nat_mul_comm]; ...)` and the renderer hides details just like you'd write "obviously" in a traditional text. If the reader wants, they could then expand the details. etc. I found that many codex-generated proofs could be improved by telling it that I want a sequence of steps

  have next_step := by <I don't care>
  have therefore := by <still don't care>
So that the human proof appears as the left side, and I just ignore the right side as petty details. Again, not fantastic success, but better. Otherwise it goes very... Leanish by default.

Lean's VSCode plugin is I think only starting to explore the idea of a proper IDE for math. There's probably still tons of unexplored potential for like that fused with Matlab or whatever.