Skip to content
Please note that GitHub no longer supports Internet Explorer.

We recommend upgrading to the latest Microsoft Edge, Google Chrome, or Firefox.

Learn more
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time. Cannot retrieve contributors at this time
30 lines (16 sloc) 5.27 KB

Maths challenges for the Lean curious

If you have played through the natural number game and are wondering what other mathematics can be done in Lean, you might want to try some of these challenges. I will try and post a few per week. The hints are essential if you are a beginner; there are no spoilers in them.

Challenge 1 (9/12/19): the composite of injective functions is injective. There's hints and the solution.

Challenge 2 (12/12/19): a set of reals has at most one supremum. There's hints and the solution.

Challenge 3 (18/12/19) : two add two isn't five. There's hints and the solution.

Challenge 4 (20/12/19) : If (g o f) is surjective then so is g. There's hints and the solution.

Challenge 5 (23/12/19) : The sum of the first n positive odd numbers is n^2. There's hints and the solution.

Challenge 6 (28/12/19) : An equivalence class for an equivalence relation is non-empty. There's hints and the solution.

Challenge 7 (9/1/20) : Is there a rational number whose reciprocal is zero? There's hints and the solution.

Challenge 8 (14/1/20) : (ghk^{-1})^{-1}=kh^{-1}g^{-1} in a group. There's hints and the solution.

Challenge 9 (22/1/20) : V(I(V(S))) = V(S) in the theory of algebraic varieties (or in any Galois connection). There's hints and the solution.

Stuck?

If you don't want to look at the solution but have questions, you can ask questions in the #new members stream on the Lean Zulip Chat (login required, real names preferred, be nice).

Here are the Lean files for the questions and solutions.

Link to this page: tinyurl.com/LeanMathsChallenges

You can’t perform that action at this time.