I was solving 2247D1 - XOR Sorting (Easy Version). My solution is as follows: for each number in the array, take the XOR of its original index and its index in the (in-place) sorted array; the answer is the largest power of two that is smaller than the maximum of these XORs. Here are two submissions that implement this logic: 385482647 385482343. The first one passes fine but the second one gives MLE. The only difference is in how I find the second index. In the first one, I just use some sorting trick. In the second one, I maintain a map<int, queue<int>> from numbers to the queue of indices. Is the overhead that large to cause MLE or am I missing something else?

Hi Codeforces!

A few months ago I announced a project: Proof-based Competitive Math Online Judge. Today, I am happy to invite you to participate in the first Week Long Practice Contest which starts on Sunday, March 1st, 2026 at 00:00 UTC and will be going for the whole week! The contest is available here . In case you haven't seen the original announcement, here is the main idea:

Lean is a special programming language that allows one to write mathematical proofs on a computer. Lean Online Judge (this project) offers math problems and accepts solutions written in Lean. Here is an example problem from the website:

Note that you are asked not only to provide an answer but also prove its correctness. The proof is checked automatically by the Lean's compiler.

If you are new to Lean, the first few chapters of Mathematics in Lean should be enough to get started. Since learning is the primary goal of the contest, problem discussion is not only allowed but encouraged. Feel free to ask any questions here or on the Discord server .

Would love too see you participate! Thanks!

UPDATE: (See the original project announcement below)

It took some time but the proof of concept is now online (hooray!): https://leanoj.org/. You can register and give some of the problems a try. As an example, here is a solution to problem C:

import Mathlib.Algebra.Ring.Parity

theorem solution (k : ℕ) (hk : Even k) : 2 ∣ 3 ^ k + 1 ∧ ¬ 4 ∣ 3 ^ k + 12 := by
  rw [even_iff_exists_two_mul] at hk
  obtain ⟨n, rfl⟩ := hk
  constructor
  · simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.pow_mod]
  · simp [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, pow_mul, Nat.pow_mod]

There are many high-quality resources on different aspects of Lean you can find here. The first few chapters of Mathematics in Lean should be enough to get started. I am also planning to make tutorials on Lean specifically for competitive math. If you are experienced in Lean or in competitive math and want to help, please, let me know.

I created a Discord server that everyone is welcome to join! This can be used to discuss anything related to the project, Lean, and math olympiads. Future updates will also be made there. Cheers!

Hi Codeforces!

Almost a year ago, I wrote a short blog post asking whether it is possible to host online math competitions in a style similar to Codeforces. The main requirement for the platform I envision is that it should be proof-based (since it is a competitive math platform) AND support automated submission checking (since it is an online judge). While there are awesome projects like Project Euler and MathDash, to the best of my knowledge, none of the existing platforms fulfill both parts of this requirement.

The proposal I had was to use so called proof assistants such as Lean that allow one to type in mathematical proofs in a formal language and automatically check their correctness. The original question asked whether these systems were mature enough for the task. Since then I learned that they are mature enough for way more than that. In particular, Lean has been used to formalize contemporary research-level mathematics [1, 2]!

Now, it's not as ideal as it may seem...

Lean's mathematics library Mathlib is meant to be used for advanced math and it strives for extremely high level of generality. For this and other reasons, formalizing proofs is highly non-trivial in general, and formalizing solutions in a contest environment in "real time" is practically impossible. One could develop a specialized Lean library for competitive math, but this is a huge undertaking for a single person, and with my limited experience with Lean, the whole idea kind of stalled.

Well, if no one does it, it will never happen...

I still believe such a platform would be a major boost to both competitive math and proof assistant communities. For now, I am planning to build an online judge using Mathlib ignoring previously mentioned concerns. If things go well and there are enough people interested, the new competitive math library could then become a community-driven project (just like Mathlib), making the goal much more feasible. I'm writing this post mainly to hold myself accountable but if you have any ideas or suggestions, please, feel free to share.

I will write a new post when there is some progress to share. Thank you!

So I was wondering if it is possible to host math competitions in a way similar to Codeforces. The obvious difficulty would be checking the solutions, since they are normally written in a natural language, meaning they cannot be checked automatically (at least yet). However, there are programming languages/proof assistants such as [Lean](https://en.wikipedia.org/wiki/Lean_(proof_assistant)) allowing you to write mathematical proofs that can be verified by a computer. I am not actually familiar with any of them, so I have two questions:

1. Are these languages mature enough or can become mature enough in the nearest future to host math competitions similar to the style of Codeforces.
2. As far as I know, doing math on a computer is still quite a niche thing in the math community. Do you think such competitions could make it more popular?

My reasoning is that a working mathematician might be reluctant to start using Lean, since there is no immediate personal benefit. However, students would be more willing to try for the sake of competitions, and then continue using it in academia in the future.

My slow solution 291665439 to 2031D - Penchick and Desert Rabbit passes the system tests.

My submission 148630829 for 1646D - Weight the Tree.

Jury's answer and the checker comment for Test 6.