add problem statements for Imo1983P3, Imo1995P6, Imo1999P2

Author: dwrensha

Compfiles.lean

@@ -83,6 +83,7 @@ import Compfiles.Imo1982P1
 import Compfiles.Imo1982P3
 import Compfiles.Imo1982P4
 import Compfiles.Imo1983P1
+import Compfiles.Imo1983P3
 import Compfiles.Imo1983P5
 import Compfiles.Imo1983P6
 import Compfiles.Imo1984P1
@@ -121,6 +122,7 @@ import Compfiles.Imo1994P4
 import Compfiles.Imo1994P5
 import Compfiles.Imo1994P6
 import Compfiles.Imo1995P2
+import Compfiles.Imo1995P6
 import Compfiles.Imo1995P4
 import Compfiles.Imo1996P3
 import Compfiles.Imo1996P4
@@ -132,6 +134,7 @@ import Compfiles.Imo1998P2
 import Compfiles.Imo1998P3
 import Compfiles.Imo1998P4
 import Compfiles.Imo1998P6
+import Compfiles.Imo1999P2
 import Compfiles.Imo1999P3
 import Compfiles.Imo1999P4
 import Compfiles.Imo1999P6

Compfiles/Imo1983P3.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 The Compfiles Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors:
+-/
+
+import Mathlib.Tactic
+
+import ProblemExtraction
+
+problem_file { tags := [.NumberTheory] }
+
+/-!
+# International Mathematical Olympiad 1983, Problem 3
+
+Let a, b, c be positive integers, no two of which have a common divisor
+greater than 1. Show that 2abc − ab − bc − ca is the largest integer
+which cannot be expressed in the form xbc + yca + zab, where x, y, z
+are non-negative integers.
+-/
+
+namespace Imo1983P3
+
+problem imo1983_p3 (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
+    (hab : Nat.Coprime a b) (hbc : Nat.Coprime b c) (hca : Nat.Coprime c a) :
+    IsGreatest
+      {n : ℤ | ¬∃ x y z : ℕ, n = x * (b * c) + y * (c * a) + z * (a * b)}
+      (2 * a * b * c - a * b - b * c - c * a) := by
+  sorry
+
+end Imo1983P3

Compfiles/Imo1995P6.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 The Compfiles Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors:
+-/
+
+import Mathlib.Tactic
+
+import ProblemExtraction
+
+problem_file { tags := [.Combinatorics, .NumberTheory] }
+
+/-!
+# International Mathematical Olympiad 1995, Problem 6
+
+Let p be an odd prime number. How many p-element subsets A of
+{1, 2, ..., 2p} are there, the sum of whose elements is
+divisible by p?
+-/
+
+namespace Imo1995P6
+
+determine solution (p : ℕ) : ℕ := sorry
+
+problem imo1995_p6 (p : ℕ) (hp : p.Prime) (hodd : Odd p) :
+    (((Finset.Icc 1 (2 * p)).powersetCard p).filter
+      (fun A ↦ p ∣ ∑ x ∈ A, x)).card = solution p := by
+  sorry
+
+end Imo1995P6

Compfiles/Imo1999P2.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 The Compfiles Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors:
+-/
+
+import Mathlib.Tactic
+
+import ProblemExtraction
+
+problem_file { tags := [.Algebra, .Inequality] }
+
+/-!
+# International Mathematical Olympiad 1999, Problem 2
+
+Let n ≥ 2 be a fixed integer. Find the least constant C such that
+
+  ∑_{i < j} xᵢxⱼ(xᵢ² + xⱼ²) ≤ C (∑ i, xᵢ)⁴
+
+for all non-negative real numbers x₁, ..., xₙ.
+-/
+
+namespace Imo1999P2
+
+determine C : ℝ := sorry
+
+problem imo1999_p2 (n : ℕ) (hn : 2 ≤ n) :
+    IsLeast
+      {c : ℝ | ∀ x : Fin n → ℝ, (∀ i, 0 ≤ x i) →
+        ∑ i, ∑ j ∈ Finset.Ioi i, x i * x j * ((x i) ^ 2 + (x j) ^ 2) ≤
+          c * (∑ i, x i) ^ 4}
+      C := by
+  sorry
+
+end Imo1999P2