Fix definition dependency & Sort jsonl

[subfish-zhou]

My previous commit (#6) didn't add the definition of the theorem dependencies. I've fixed it now. Sorry, it was a serious mistake.

PR #7 points out that the jsonl file might be out of order and there was a missing log file for the script. I’ve added sorting to the script so the jsonl entries are now arranged in lexicographic order. I also added the log file to .gitignore, so we don’t have to worry about it anymore.

There are two other things I want to discuss:

1. The ProofNetSharp project splits the dataset into valid and test sets, similar to MiniF2F. If users want to make use of that split, they can try this project. However, ProofNetSharp is missing Cambridge-Tripos.lean.

2. I saw that some statements declared in instance. In fact, they can all be converted into theorems completely equivalently by adding a predicate Nonempty. Here is an example from Dummit-Foote.lean:

instance exercise_1_6_11 {A B : Type*} [Group A] [Group B] : A × B ≃* B × A := sorry

theorem exercise_1_6_11' {A B : Type*} [Group A] [Group B] : Nonempty (A × B ≃* B × A) := by sorry

Even the proofs are exactly the same. I'm not sure if we need to unify all the data into theorem.