I would be glad to try this new area (theorem proving) as well as new (non-traditional) programming languages.
My opinion that 8kyu should be like the starting point, shouldn't it? But instead of simple stuff to get in touch with new ideas and approaches, I find hard tasks that forces me to read a book. I would like to see like step by step tasks. Otherwise this becomes very useless when the only people who can solve it the ones who worked with this before

It's totally crazy... I don't want to spend hours reading a text to solve "the easiest" task.
Actually I don't find anything hard in what I read, despite this I cannot solve it. It does not even make me thinking about anything, just getting info...

Are you kidding applying 8kyu to it?
I've read some chapters of this work: https://softwarefoundations.cis.upenn.edu/current/lf-current/toc.html and could not imaging how to prove it.
I've taken a look at lean and it looks even more tricky

It can consume huge amount of memory, right?

I don't know why this does not work, maybe the bug is already fixed in the version I use locally.
But I've found another solution that works locally as well as here :)

It works locally, but not here. With Kotlin 1.2 there is NPE in String class and with 1.3 I get:
exception: java.lang.IllegalStateException: Backend Internal error: Exception during code generation
Cause: Back-end (JVM) Internal error: wrong code generated
org.jetbrains.kotlin.codegen.CompilationException Back-end (JVM) Internal error: Couldn't transform method node:
testInt ()V:
@Lorg/junit/Test;()
L0
LINENUMBER 8 L0
NEW java/util/Random
DUP
INVOKESTATIC java/lang/System.currentTimeMillis ()J
INVOKESPECIAL java/util/Random. (J)V
ASTORE 1
L1
LINENUMBER 9 L1
ICONST_0
ISTORE 2
NEW kotlin/ranges/IntRange
DUP
ILOAD 2
BIPUSH 100
INVOKESPECIAL kotlin/ranges/IntRange. (II)V
.......

transform method is really helpful, good approach, thanks :)

Trying to attempt
/workspace/java/src/UserTest.java:7: error: reference to assertEquals is ambiguous
assertEquals("After applying rank of " + rank + " the resulting user rank was expected to be " + expectedRank + ", but was actually " + user.rank, expectedRank, user.rank);
^
both method assertEquals(String,long,long) in Assert and method assertEquals(String,Object,Object) in Assert match
/workspace/java/src/UserTest.java:8: error: reference to assertEquals is ambiguous
assertEquals("After applying rank of " + rank + " the progress was expected to be " + expectedProgress + ", but was actually " + user.progress, expectedProgress, user.progress);
^
both method assertEquals(String,long,long) in Assert and method assertEquals(String,Object,Object) in Assert match
2 errors

dirty