> On May 7, 2023, at 12:23 PM, Jon P <[email protected]> wrote:
> Re this one thing I wondered about is whether adding english text between the
> statements might help a language model understand what is happening? It would
> be very repetitive so maybe it makes no sense but here is an example. ...
The underlying Metamath proof format *does* support comments internal to the
proof.
See the Metamath book appendix E ("Metamath Language EBNF").
However, in *practice* tools don't use that information to generate output, nor
do they
take any steps to keep such comments. I'm not sure anyone is seriously
interested in processing them.
Maybe we should, but then we'd have to think about how to handle changes.
> I think maybe that makes it easier to understand what is happening and gives
> the language model something to grip on to which training?
Perhaps, but no one's trying to do that. Currently, if there's a trickiness,
it's documented in the high-level description of the statement as a whole. If
if's more sophisticated, it might be better split out as its own theorem.
--- David A. Wheeler
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/42E62100-7A9C-4B2E-BC50-7D82E6F62F5A%40dwheeler.com.
