1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24

def gcd (a b : Nat) : Nat :=
  if b > 0 then gcd b (a % b) else a
termination_by b
decreasing_by
  exact Nat.mod_lt a ‹_›

def N := 1000

def A := Array.range N

def sum := (A.map fun x ↦ A.map (gcd x ·) |>.sum).sum

-- def T := 8

-- def sum := (Task.mapList List.sum <| A.toList.map fun x ↦ (Task.spawn fun _ ↦ A.map (gcd x ·) |>.sum)) |>.get

-- def sum :=
--   (Task.mapList List.sum <| List.range T |>.map fun t ↦
--     (Task.spawn fun _ ↦ (A[N/T*t:N/T*(t+1)].toArray.map fun x ↦ A.map (gcd x ·) |>.sum).sum)
--   ).get

def main := do
  IO.println "test"
  IO.println sum