warning: PrimeNumberTheoremAnd: repository '/home/proof/active/.lake/packages/PrimeNumberTheoremAnd' has local changes
warning: belyi: repository '/home/proof/active/.lake/packages/belyi' has local changes
warning: formal-schemes: repository '/home/proof/active/.lake/packages/formal-schemes' has local changes
warning: elliptic-curves: repository '/home/proof/active/.lake/packages/elliptic-curves' has local changes
warning: tempered-fundamental-groups: repository '/home/proof/active/.lake/packages/tempered-fundamental-groups' has local changes
warning: oka: repository '/home/proof/active/.lake/packages/oka' has local changes
warning: orbicurve-cores: repository '/home/proof/active/.lake/packages/orbicurve-cores' has local changes
warning: pi1: repository '/home/proof/active/.lake/packages/pi1' has local changes
warning: heights: repository '/home/proof/active/.lake/packages/heights' has local changes
warning: genl: repository '/home/proof/active/.lake/packages/genl' has local changes
warning: tate-curves-theta: repository '/home/proof/active/.lake/packages/tate-curves-theta' has local changes
warning: iut: repository '/home/proof/active/.lake/packages/iut' has local changes
warning: gromov: repository '/home/proof/active/.lake/packages/gromov' has local changes
warning: SphereEversion: repository '/home/proof/active/.lake/packages/SphereEversion' has local changes
warning: schoenflies-lean: repository '/home/proof/active/.lake/packages/schoenflies-lean' has local changes
warning: ClassFieldTheory: repository '/home/proof/active/.lake/packages/ClassFieldTheory' has local changes
warning: AINTLIB: repository '/home/proof/active/.lake/packages/AINTLIB' has local changes
warning: AbsorptionCutoff: repository '/home/proof/active/.lake/packages/AbsorptionCutoff' has local changes
warning: StrongPNT: repository '/home/proof/active/.lake/packages/StrongPNT' has local changes
warning: carleson: repository '/home/proof/active/.lake/packages/carleson' has local changes
warning: rellich-kondrachov: repository '/home/proof/active/.lake/packages/rellich-kondrachov' has local changes
warning: Zeta3Irrational: repository '/home/proof/active/.lake/packages/Zeta3Irrational' has local changes
warning: fixed-point-theorems: repository '/home/proof/active/.lake/packages/fixed-point-theorems' has local changes
Building ComparatorChallenges.AbhyankarSathaye
warning: PrimeNumberTheoremAnd: repository '/home/proof/active/.lake/packages/PrimeNumberTheoremAnd' has local changes
warning: belyi: repository '/home/proof/active/.lake/packages/belyi' has local changes
warning: formal-schemes: repository '/home/proof/active/.lake/packages/formal-schemes' has local changes
warning: elliptic-curves: repository '/home/proof/active/.lake/packages/elliptic-curves' has local changes
warning: tempered-fundamental-groups: repository '/home/proof/active/.lake/packages/tempered-fundamental-groups' has local changes
warning: oka: repository '/home/proof/active/.lake/packages/oka' has local changes
warning: orbicurve-cores: repository '/home/proof/active/.lake/packages/orbicurve-cores' has local changes
warning: pi1: repository '/home/proof/active/.lake/packages/pi1' has local changes
warning: heights: repository '/home/proof/active/.lake/packages/heights' has local changes
warning: genl: repository '/home/proof/active/.lake/packages/genl' has local changes
warning: tate-curves-theta: repository '/home/proof/active/.lake/packages/tate-curves-theta' has local changes
warning: iut: repository '/home/proof/active/.lake/packages/iut' has local changes
warning: gromov: repository '/home/proof/active/.lake/packages/gromov' has local changes
warning: SphereEversion: repository '/home/proof/active/.lake/packages/SphereEversion' has local changes
warning: schoenflies-lean: repository '/home/proof/active/.lake/packages/schoenflies-lean' has local changes
warning: ClassFieldTheory: repository '/home/proof/active/.lake/packages/ClassFieldTheory' has local changes
warning: AINTLIB: repository '/home/proof/active/.lake/packages/AINTLIB' has local changes
warning: AbsorptionCutoff: repository '/home/proof/active/.lake/packages/AbsorptionCutoff' has local changes
warning: StrongPNT: repository '/home/proof/active/.lake/packages/StrongPNT' has local changes
warning: carleson: repository '/home/proof/active/.lake/packages/carleson' has local changes
warning: rellich-kondrachov: repository '/home/proof/active/.lake/packages/rellich-kondrachov' has local changes
warning: Zeta3Irrational: repository '/home/proof/active/.lake/packages/Zeta3Irrational' has local changes
warning: fixed-point-theorems: repository '/home/proof/active/.lake/packages/fixed-point-theorems' has local changes
⚠ [1457/1457] Built ComparatorChallenges.AbhyankarSathaye (8.2s)
warning: ComparatorChallenges/AbhyankarSathaye.lean:11:8: declaration uses `sorry`
Build completed successfully (1457 jobs).
Exporting #[Quot, Quot.mk, Quot.lift, Quot.ind, OAI.AbhyankarSathaye.exists_noncoordinate_polynomial, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, Nat, String, String.mk, Char, optParam, autoParam, semiOutParam, outParam] from ComparatorChallenges.AbhyankarSathaye
Building OAI.AlgebraicGeometry.AbhyankarSathaye.Counterexample
warning: PrimeNumberTheoremAnd: repository '/home/proof/active/.lake/packages/PrimeNumberTheoremAnd' has local changes
warning: belyi: repository '/home/proof/active/.lake/packages/belyi' has local changes
warning: formal-schemes: repository '/home/proof/active/.lake/packages/formal-schemes' has local changes
warning: elliptic-curves: repository '/home/proof/active/.lake/packages/elliptic-curves' has local changes
warning: tempered-fundamental-groups: repository '/home/proof/active/.lake/packages/tempered-fundamental-groups' has local changes
warning: oka: repository '/home/proof/active/.lake/packages/oka' has local changes
warning: orbicurve-cores: repository '/home/proof/active/.lake/packages/orbicurve-cores' has local changes
warning: pi1: repository '/home/proof/active/.lake/packages/pi1' has local changes
warning: heights: repository '/home/proof/active/.lake/packages/heights' has local changes
warning: genl: repository '/home/proof/active/.lake/packages/genl' has local changes
warning: tate-curves-theta: repository '/home/proof/active/.lake/packages/tate-curves-theta' has local changes
warning: iut: repository '/home/proof/active/.lake/packages/iut' has local changes
warning: gromov: repository '/home/proof/active/.lake/packages/gromov' has local changes
warning: SphereEversion: repository '/home/proof/active/.lake/packages/SphereEversion' has local changes
warning: schoenflies-lean: repository '/home/proof/active/.lake/packages/schoenflies-lean' has local changes
warning: ClassFieldTheory: repository '/home/proof/active/.lake/packages/ClassFieldTheory' has local changes
warning: AINTLIB: repository '/home/proof/active/.lake/packages/AINTLIB' has local changes
warning: AbsorptionCutoff: repository '/home/proof/active/.lake/packages/AbsorptionCutoff' has local changes
warning: StrongPNT: repository '/home/proof/active/.lake/packages/StrongPNT' has local changes
warning: carleson: repository '/home/proof/active/.lake/packages/carleson' has local changes
warning: rellich-kondrachov: repository '/home/proof/active/.lake/packages/rellich-kondrachov' has local changes
warning: Zeta3Irrational: repository '/home/proof/active/.lake/packages/Zeta3Irrational' has local changes
warning: fixed-point-theorems: repository '/home/proof/active/.lake/packages/fixed-point-theorems' has local changes
✔ [1604/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Identities (3.0s)
✔ [1605/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Quotient (2.9s)
✔ [1606/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.LiftingIdentities (2.9s)
✔ [1607/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.CriticalPoint (2.0s)
✔ [1608/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Reconstruction (4.2s)
✔ [1609/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.LinearElimination (4.2s)
✔ [1610/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.NonCoordinate (4.5s)
✔ [1611/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Plane (5.1s)
✔ [1612/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Lifting (3.5s)
✔ [1613/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Presentation (4.2s)
✔ [1614/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.LinearPresentation (4.2s)
✔ [1615/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Fiber (3.9s)
✔ [1616/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Stabilization (3.0s)
✔ [1617/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.FiberFormulas (3.4s)
✔ [1618/1618] Built OAI.AlgebraicGeometry.AbhyankarSathaye.Counterexample (2.0s)
Build completed successfully (1618 jobs).
Exporting #[Quot, Quot.mk, Quot.lift, Quot.ind, OAI.AbhyankarSathaye.exists_noncoordinate_polynomial, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, Nat, String, String.mk, Char, optParam, autoParam, semiOutParam, outParam] from OAI.AlgebraicGeometry.AbhyankarSathaye.Counterexample
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!