Search results

Use closeMainGoalUsing in Pratt tactic

enhancementNew feature or requestNew feature or request

good first issueGood for newcomersGood for newcomers

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#134 In Verified-zkEVM/CompPoly;

· dhsorens opened on Feb 27, 2026

Define computable Additive NTT and transfer correctness

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#132 In Verified-zkEVM/CompPoly;

· dhsorens opened on Feb 27, 2026

Migrate concreteTowerAlgebraMap recursion to Fin.dfoldl

enhancementNew feature or requestNew feature or request

good first issueGood for newcomersGood for newcomers

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#131 In Verified-zkEVM/CompPoly;

· dhsorens opened on Feb 27, 2026

Migrate towerAlgebraMap recursion to Fin.dfoldl

enhancementNew feature or requestNew feature or request

good first issueGood for newcomersGood for newcomers

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#130 In Verified-zkEVM/CompPoly;

· dhsorens opened on Feb 27, 2026

Optimize clMul in Binary Common

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#129 In Verified-zkEVM/CompPoly;

· dhsorens opened on Feb 27, 2026

Implement finSuccEquiv and optionEquivLeft for CMvPolynomial

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

phase 1 - theoryPhase 1 of the roadmap, focusing on theory completenessPhase 1 of the roadmap, focusing on theory completeness

Status: Open.

#93 In Verified-zkEVM/CompPoly;

· dhsorens opened on Feb 16, 2026

Implement Algebra and Module instances for CMvPolynomial

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

phase 1 - theoryPhase 1 of the roadmap, focusing on theory completenessPhase 1 of the roadmap, focusing on theory completeness

Status: Open.

#91 In Verified-zkEVM/CompPoly;

· dhsorens opened on Feb 16, 2026

Clarify and implement <code>sumToIter</code>

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

phase 1 - theoryPhase 1 of the roadmap, focusing on theory completenessPhase 1 of the roadmap, focusing on theory completeness

Status: Open.

#56 In Verified-zkEVM/CompPoly;

· dhsorens opened on Jan 21, 2026

Implement <code>CommRing</code> instance for <code>CMvPolynomial</code>

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

phase 1 - theoryPhase 1 of the roadmap, focusing on theory completenessPhase 1 of the roadmap, focusing on theory completeness

Status: Open.

#55 In Verified-zkEVM/CompPoly;

· dhsorens opened on Jan 21, 2026

Implement algebra evaluation and substitution: <code>aeval</code> and <code>bind₁</code>

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

phase 1 - theoryPhase 1 of the roadmap, focusing on theory completenessPhase 1 of the roadmap, focusing on theory completeness

Status: Open.

#52 In Verified-zkEVM/CompPoly;

· dhsorens opened on Jan 21, 2026

Implement monomial ordering functions: <code>MonomialOrder.degree</code>, <code>leadingMonomial</code>, <code>leadingCoeff</code>

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

phase 1 - theoryPhase 1 of the roadmap, focusing on theory completenessPhase 1 of the roadmap, focusing on theory completeness

Status: Open.

#49 In Verified-zkEVM/CompPoly;

· dhsorens opened on Jan 21, 2026

Implement computable versions of degreeLT, degreeLE, and related membership lemmas

enhancementNew feature or requestNew feature or request

help wantedExtra attention is neededExtra attention is needed

phase 1 - theoryPhase 1 of the roadmap, focusing on theory completenessPhase 1 of the roadmap, focusing on theory completeness

Status: Open.

#48 In Verified-zkEVM/CompPoly;

· dhsorens opened on Jan 21, 2026