Bugs in Metamath Problem Statements

[XiaoHLim]

Hi, I encountered a few issues in the Metamath problem statements:

1. miniF2F/metamath/valid/amc12a-2002-p21.mm

   Lines 1 to 11 in 4e433ff

   	$(
   	@{
   	amc12a-2002-p21.0 @e |- ( ph -> U : NN --> NN0 ) $@
   	amc12a-2002-p21.1 @e |- ( ph -> ( U ` 1 ) = 4 ) $@
   	amc12a-2002-p21.2 @e |- ( ph -> ( U ` 2 ) = 7 ) $@
   	amc12a-2002-p21.3 @e |- ( ph -> A. n e. ( ZZ>= ` 3 ) ( U ` ( n + 2 ) ) = ( ( ( U ` n ) + ( U ` ( n + 1 ) ) ) mod 10 ) ) $@
   	@( (Contributed by Kunhao Zheng, 4-May-2021.) @)
   	amc12a-2002-p21 @p |- ( ph -> ( A. n e. NN sum_ k e. ( 1 ... N ) ( U ` k ) > ; ; ; ; 1 0 0 0 0 -> ; ; ; 1 9 9 9 <_ n ) ) @=
   	? @.
   	@}
   	$)

   
   where 10 in L6 is an unknown token. It should be corrected to ; 1 0.

2. miniF2F/metamath/test/aime-1983-p1.mm

   Lines 1 to 17 in 4e433ff

   	$(
   	@{
   	aime-1983-p1.0 @e |- ( ph -> X e. NN ) $@
   	aime-1983-p1.1 @e |- ( ph -> Y e. NN ) $@
   	aime-1983-p1.2 @e |- ( ph -> Z e. NN ) $@
   	aime-1983-p1.3 @e |- ( ph -> 1 < X ) $@
   	aime-1983-p1.4 @e |- ( ph -> 1 < Y ) $@
   	aime-1983-p1.5 @e |- ( ph -> 1 < Z ) $@
   	aime-1983-p1.6 @e |- ( ph -> W e. NN0 ) $@
   	aime-1983-p1.7 @e |- ( ph -> ( X logb W ) = ; 2 4 ) $@
   	aime-1983-p1.8 @e |- ( ph -> ( Y logb W ) = ; 4 0 ) $@
   	aime-1983-p1.9 @e |- ( ph -> ( ( X x. ( Y x. Z ) ) logb W ) = ; 1 2 ) $@
   	$@ (Contributed by Kudzo Ahegbebu, 28-Jun-2021.) $@
   	aime-1983-p1 @p |- ( ph -> ( Z logb W ) = ; 6 0 ) @=
   	? @.
   	@}
   	$)

   
   where $@ in L13 is incorrectly used for comments. According to the convention in other problems, it should be @( and @).

3. miniF2F/metamath/test/aime-1994-p3.mm

   Lines 1 to 11 in 4e433ff

   	$(
   	@{
   	aime-1994-p3.0 @e |- ( ph -> X e. RR ) $@
   	aime-1994-p3.1 @e |- ( ph -> F : RR --> RR ) $@
   	aime-1994-p3.2 @e |- ( ph -> ( ( F ` X ) + ( F ` ( X + 1 ) ) ) = ( X ^ 2 ) ) $@
   	aime-1994-p3.3 @e |- ( ph -> ( F ` ; 1 9 ) = ; 9 4 ) $@
   	@( (Contributed by Kudzo Ahegbebu, 28-Jun-2021.) @)
   	aime-1994-p3.3 @p |- ( ph -> ( ( F ` ; 9 4 ) mod ; ; ; 1 0 0 0 ) = ; ; 5 6 1 ) @=
   	? @.
   	@}
   	$)

   
   where aime-1994-p3.3 is multiply defined. It should be standardized to aime-1994-p3 as per Metamath conventions.

[DyeKuu]

Hi @XiaoHLim! Thank you for spotting this. Unfortunately I don't have too much bandwidth for setting up mm environment now and fix this. Do you think you could open a PR to https://github.com/facebookresearch/miniF2F to fix the metamath statement? I don't think this repo is maintained by anyone now. Thank you very much!