Formalizing "Real Analysis" by Jay Cummings

Stream: maths

[TauTastic]

I'm currently working on formalizing the exercises from Jay Cummings' "Real Analysis" book. You can find my progress so far on GitHub: Real Analysis Exercises Repository.

Feel free to check it out. Contributions are welcome!

[Jireh Loreaux]

@TauTastic I'm not sure what your goals are vis-a-vis whether you allow access to Mathlib theorems, but I assume you do. Note that all but three of the question from your "Chapter 1: Basic" are solved by exact?%. Also, the last question seems unlikely to be formalized correctly (I think you likely want ∧ not →).

[Jireh Loreaux]

For the other three:

/-Exercise 1.5 c-/
theorem diff_eq_left (A B : Set α) : A \ B = A ↔ A ∩ B = ∅ := by
  rw [sdiff_eq_left, Set.disjoint_iff_inter_eq_empty]

/-Exercise 1.10-/
theorem mul_id_unique {F : Type*} [Field F] {e1 e2 : F}
(h1 : ∀ x : F, e1 * x = x) (h2 : ∀ x : F, e2 * x = x) : e1 = e2 := by
  simpa using (h1 1).trans (h2 1).symm

/-Exercise 1.12 b-/
theorem not_necessarily_lt_mul {F : Type*} [LinearOrderedField F] :
(∃ a b c d : F, a < b ∧ c < d ∧ b * d ≤ a * c) := by
  use -1, 0, -1, 0
  refine ⟨?_, ?_, ?_⟩
  all_goals norm_num

[TauTastic]

Thanks for the correction on the last exercise. Regarding your question about allowing Mathlib theorems: I am not quite sure yet what the best approach would be. Currently, I am only formalizing the exercises so people can solve them however they want. Ideally, if I had enough time, I would like to build a game, like the Natural Number Game or Robo, using the exercises from the book. To do so, I would have to decide which theorems the user has to prove before they can use them and which ones can be used from the start.

If you have any thoughts, feel free to contribute or open issues in the repo :)

[Yury G. Kudryashov]

Another possible goal is to make sure that Mathlib has all theorems needed to solve problems from this textbook.