Issues

• goal_commentshas no effect

  kim-em/lean-training-data#8 · Filter by author zzhisthebest opened on Mar 28, 2025
  1

• uncaught exception error

  kim-em/lean-training-data#7 · Filter by author zzhisthebest opened on Mar 28, 2025
  1

• install problems

  kim-em/lean-training-data#6 · Filter by author FrederickPu opened on Feb 11, 2025
  1

• tactic_benchmark fails when file contains sorry

  kim-em/lean-training-data#3 · Filter by author zhangir-azerbayev opened on Jan 24, 2024

• Changing mathlib version and a couple questions

  kim-em/lean-training-data#1 · Filter by author AG161 opened on Nov 7, 2023