NKS page 778:
In[]:=
ResourceFunction["MultiwaySystem"][{"A""BAB","BB""A","AA""B"},{"BAB"},4]
Out[]=
{{BAB},{BBABB},{AABB,BBAA,BBBABBB},{AAA,ABABBB,BAABBB,BABABB,BBABAB,BBB,BBBAAB,BBBABA,BBBBABBBB},{AABAB,AB,ABAAB,ABABA,ABBABBBB,BA,BAAAB,BAABA,BABAA,BABABBBB,BABBABBB,BBAABBBB,BBABABBB,BBABBABB,BBBABABB,BBBABBAB,BBBBAABB,BBBBABAB,BBBBABBA,BBBBB,BBBBBABBBBB}}
In[]:=
FindStringReplacePath[{"A""BAB","BB""A","AA""B"},"A","AA"]
Out[]=
{A,BAB,BBABB,AABB,ABABBB,ABBABBBB,AAABBBB,AAAABB,AAAAA,AAAB,ABB,AA}
In[]:=
FindStringReplacePath[{"A""BAB","BB""A","AA""B"},"B","A"]
Out[]=
Failure

Message:
Number of states reached
12451
Tag:
toobig

In[]:=
FindStringReplacePath[{"A""BAB","BB""A","AA""B"},"A","B"]
Out[]=
{A,BAB,BBABB,AABB,ABABBB,ABBABBBB,AAABBBB,AAAABB,AAAAA,AAAB,ABB,AA,B}

NKS proof length examples

https://www.wolframscience.com/nks/p796--implications-for-mathematics-and-its-foundations/
Out[]=
{{BBB,BBB},{BAA,AAAB},{BABA,A},{BBB,BBA},{BABA,AAB,BBA},{BABA,AAB,BBAB},{BBAB,ABABB,BBAA},{BBA,BAAABB,BABB}}
In[]:=
strings=(StringJoin[#/.{1"B",0"A"}])&/@Rest/@IntegerDigits[Range[2,31],2]
Out[]=
{A,B,AA,AB,BA,BB,AAA,AAB,ABA,ABB,BAA,BAB,BBA,BBB,AAAA,AAAB,AABA,AABB,ABAA,ABAB,ABBA,ABBB,BAAA,BAAB,BABA,BABB,BBAA,BBAB,BBBA,BBBB}
In[]:=
Function[ru,FindStringReplacePath[ru,"B",#,MaxItems1000]&/@strings]/@{{"B""BB","BB""B"},{"B""AA","AA""AB"},{"B""ABA","A"""},{"B""BB","BB""A"},{"B""ABA","AA""B","BB""A"},{"B""ABA","AA""B","BB""AB"},{"B""BAB","ABAB""B","BB""AA"},{"B""BA","BAA""ABB","BAB""B"}}
Out[]=
$Aborted
In[]:=
Function[ru,FindStringReplacePath[ru,"B",#,MaxItems100,TimeConstraint2]&/@strings]/@{{"B""AA","AA""AB"}}
Out[]=
Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,{B,AA},{B,AA,AB},Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,{B,AA,AB,AAA},{B,AA,AB,AAA,AAB},{B,AA,AB,AAA,ABA},{B,AA,AB,AAA,AAB,ABB},Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,{B,AA,AB,AAA,AAB,AAAA},{B,AA,AB,AAA,AAB,AAAA,AAAB},{B,AA,AB,AAA,AAB,AAAA,AABA},{B,AA,AB,AAA,AAB,AAAA,AAAB,AABB},{B,AA,AB,AAA,AAB,AAAA,ABAA},{B,AA,AB,AAA,AAB,AAAA,AAAB,ABAB},{B,AA,AB,AAA,AAB,AAAA,AABA,ABBA},{B,AA,AB,AAA,AAB,AAAA,AAAB,AABB,ABBB},Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig
,Failure

Message:
Number of states reached
113
Tag:
toobig

In[]:=
results=Function[ru,ResourceFunction["ParallelMapMonitored"][FindStringReplacePath[ru,"B",#,MaxItems1000,TimeConstraint2]&,strings]]/@{{"B""BB","BB""B"},{"B""AA","AA""AB"},{"B""ABA","A"""},{"B""BB","BB""A"},{"B""ABA","AA""B","BB""A"},{"B""ABA","AA""B","BB""AB"},{"B""BAB","ABAB""B","BB""AA"},{"B""BA","BAA""ABB","BAB""B"}};
In[]:=
Map[If[Head[#]===Failure,Infinity,Length[#]]&,results,{2}]
Out[]=
{{∞,1,∞,∞,∞,2,∞,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4},{∞,∞,2,3,∞,∞,4,5,5,6,∞,∞,∞,∞,6,7,7,8,7,8,8,9,∞,∞,∞,∞,∞,∞,∞,∞},{∞,1,∞,3,3,∞,∞,5,2,∞,5,∞,∞,∞,∞,7,4,∞,4,∞,∞,∞,7,∞,∞,∞,∞,∞,∞,∞},{3,∞,6,4,4,2,9,7,7,5,7,5,5,3,12,10,10,8,10,8,8,6,10,8,8,6,8,6,6,4},{13,1,9,6,6,12,5,11,2,8,11,8,8,5,10,7,7,4,7,13,13,10,7,13,13,10,4,10,10,∞},{∞,1,∞,9,∞,8,∞,7,2,6,∞,6,11,5,∞,5,10,4,5,9,9,8,∞,14,9,13,4,8,8,12},{∞,1,5,10,∞,4,∞,8,∞,∞,8,2,∞,7,∞,6,∞,11,∞,11,∞,∞,6,∞,∞,5,11,5,∞,∞},{∞,1,∞,6,2,∞,∞,11,7,4,3,∞,∞,∞,∞,16,12,9,8,5,5,∞,4,∞,∞,∞,∞,∞,∞,∞}}

One Example of Shortening

In[]:=
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"StatesGraph"]
Out[]=
Consider each possible lemma; how much does it shorten the results?
In[]:=
LayeredGraphPlot[ResourceFunction["MultiwaySystem"][{"A""AB","BB""A","A""AA"},{"A"},4,"StatesGraph"]]
Out[]=

Shortening due to a particular lemma

In[]:=
Map[Length[FindStringReplacePath[{"A""AB","BB""A","A""AA"},"A",#]]&,ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},7],{2}]
Out[]=
{{1},{2},{3},{2,4},{3,3,5},{4,4,4,6},{3,5,5,5,5,7},{4,4,6,4,6,6,6,6,8}}
In[]:=
Map[Length[FindStringReplacePath[{"A""AB","BB""A","A""AA"},"A",#]]&,ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},9],{2}]
Out[]=
{{1},{2},{3},{2,4},{3,3,5},{4,4,4,6},{3,5,5,5,5,7},{4,4,6,4,6,6,6,6,8},{5,5,5,7,5,5,7,5,7,7,7,7,9},{4,6,6,6,6,8,6,6,6,8,6,6,8,6,8,8,8,8,10}}
In[]:=
MapIndexed[First[#2]-#&,%]
Out[]=
{{0},{0},{0},{2,0},{2,2,0},{2,2,2,0},{4,2,2,2,2,0},{4,4,2,4,2,2,2,2,0},{4,4,4,2,4,4,2,4,2,2,2,2,0},{6,4,4,4,4,2,4,4,4,2,4,4,2,4,2,2,2,2,0}}
In[]:=
N[Mean[#]]&/@%
Out[]=
{0.,0.,0.,1.,1.33333,1.5,2.,2.44444,2.76923,3.15789}
In[]:=
ListLinePlot[%]
Out[]=
0
2
4
6
8
10
0.5
1.0
1.5
2.0
2.5
3.0
Linear improvement with this lemma....

Consider all A ... lemmas

This looks at shortening of A... paths

Consider AA ... lemmas

The lemmas become more irrelevant if we are not looking at shortening paths that do not reach as far as they do

Bulk lemma measurements

Enumeration of Rules

What is the proof length for a particular string?

Note: see Metamath-LongProofs-01

Proof Shorteners

Lemmas are not general-purpose proof shorteners ... they only shorten in particular “direction” in metamathematical space....

If a particular lemma is going to be used on several distinct strings, it must be operating on different substrings

With enough lemmas

Terminating Rules