Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: QuantumWar

Submitted at: 2026-01-09 13:36:12

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

def solveAdd (a b : Int) : Int := 
  b - a

First Theorem Proof:

theorem solveAdd_correct (a b: Int): a + (solveAdd a b) =b 

theorem solveAdd_correct (a b : Int) : a + (solveAdd a b) = b := by
  unfold solveAdd
  rw [Int.add_comm]
  exact Int.sub_add_cancel b a

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmp37cy18s7/proof.lean:
/root/CodeProofTheArena/temp/tmp37cy18s7/proof.lean:6:27: error: unexpected token 'def'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmp37cy18s7/proof.lean:7:4: error: 'solveAdd' has already been declared
/root/CodeProofTheArena/temp/tmp37cy18s7/proof.lean:11:58: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmp37cy18s7/proof.lean:12:8: error: 'solveAdd_correct' has already been declared