Quasi-linear Time Multiplication of Sparse Polynomials with Integer Coefficients

Qiao-Long Huang; Ruichen Qiu; Xiao-Shan Gao; Yichuan Cao

arxiv: 2606.12100 · v1 · pith:QIAKHBMLnew · submitted 2026-06-10 · 💻 cs.SC · cs.CC

Quasi-linear Time Multiplication of Sparse Polynomials with Integer Coefficients

Qiao-Long Huang , Yichuan Cao , Ruichen Qiu , Xiao-Shan Gao This is my paper

Pith reviewed 2026-06-27 07:45 UTC · model grok-4.3

classification 💻 cs.SC cs.CC

keywords sparse polynomial multiplicationquasi-linear timeinteger coefficientsmodular black-box interpolationoutput-sensitive algorithmfinite field coefficientscomputer algebra

0 comments

The pith

A quasi-linear bit complexity algorithm for sparse polynomial multiplication with integer coefficients is obtained by reduction to modular black-box interpolation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tackles the open problem of quasi-linear time output-sensitive multiplication for sparse polynomials. It first supplies a counterexample disproving an earlier claimed solution in the integer-coefficient case. It then builds a new algorithm whose bit complexity is quasi-linear by treating an existing modular-black-box interpolation routine as a black box. For coefficients in a finite field the resulting bit complexity becomes linear in the number of terms together with the logarithms of the degree and the field size. A sympathetic reader would care because sparse multiplication is a core primitive in computer algebra, and an output-sensitive quasi-linear bound would make previously intractable computations feasible.

Core claim

By invoking the existing quasi-linear modular-black-box interpolation algorithm as a black box, the integer-coefficient sparse multiplication problem admits an algorithm whose bit complexity is quasi-linear in the combined size of the input and output.

What carries the argument

The modular-black-box interpolation algorithm, invoked as a black box to transfer its quasi-linear complexity to the integer-coefficient multiplication task.

If this is right

The open challenge of quasi-linear output-sensitive sparse multiplication receives a solution for integer coefficients.
For finite-field coefficients the bit complexity simplifies to linear dependence on the number of terms, the logarithm of the degree, and the logarithm of the field size.
Any future improvement to the black-box interpolation routine immediately yields a corresponding improvement to the multiplication algorithm.
The reduction shows that the integer-coefficient case can be handled without developing a new interpolation procedure from scratch.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Implementations in computer algebra systems could adopt the reduction once the underlying interpolation routine is available, potentially accelerating Gröbner-basis and resultant computations.
The same black-box reduction strategy might apply to other coefficient domains that admit efficient modular reductions, such as algebraic number fields.
If the interpolation routine itself admits a practical implementation, the multiplication algorithm could become the default method for large sparse products rather than a purely theoretical result.

Load-bearing premise

The modular-black-box interpolation procedure already runs in quasi-linear time when supplied as a black box.

What would settle it

An explicit input pair of sparse integer polynomials whose multiplication via the new algorithm requires super-quasi-linear bit operations would falsify the claim.

read the original abstract

Sparse polynomial multiplication is a fundamental problem in computer algebra and the theory of computation, and the development of a quasi-linear time output-sensitive multiplication algorithm has been posed as an open challenge. In this paper, a counterexample is provided to a previously claimed solution to this open problem for integer coefficients. By employing the existing quasi-linear modular-black-box interpolation algorithm, we are able to provide an algorithm with quasi-linear bit complexity for the integer coefficients setting. Furthermore, in the case of coefficients over a finite field, we obtain an algorithm whose bit complexity is linear in the number of terms, the logarithm of the degree, and the logarithm of the size of the finite field.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a counterexample to a prior claim and reduces the integer-coefficient case to an existing interpolation routine, but the abstract supplies neither the counterexample nor a complexity breakdown.

read the letter

The main new element is the counterexample to the earlier claimed solution for integer coefficients, plus the reduction that applies an existing quasi-linear modular black-box interpolation method to reach the target bit complexity. The finite-field case is stated as linear in the number of terms and the logs of degree and field size, which is a clean statement.

The reduction is the part that looks useful: it avoids new machinery and simply invokes published work. That keeps the contribution narrow and focused on the open problem.

The soft spot is exactly the one flagged in the stress test. The abstract mentions the counterexample but does not exhibit it, and it gives no count of black-box calls, no recurrence for bit lengths during modular reduction or lifting, and no argument that the overhead stays quasi-linear. The claim therefore rests on the assumption that the invoked routine already delivers the bound with no extra factors from the reduction steps. Without those details the complexity result cannot be checked.

The citation pattern is appropriate; it points to prior published work rather than circular self-reference.

This is a paper for people who work on sparse polynomial algorithms and the internals of computer algebra systems. A reader who needs the current best multiplication routine for integer coefficients would get value from the reduction if the missing pieces are supplied cleanly in the full text. It is the kind of targeted improvement that deserves referee time to inspect the counterexample and verify that the reduction really preserves quasi-linear bit complexity.

I would send it to peer review.

Referee Report

2 major / 0 minor

Summary. The manuscript provides a counterexample to a prior claimed quasi-linear time algorithm for sparse polynomial multiplication over the integers. It then constructs a new algorithm for the integer-coefficient case by reduction to an existing quasi-linear modular black-box interpolation procedure, claiming quasi-linear bit complexity overall. For coefficients in a finite field the claimed bit complexity is linear in the number of terms, the logarithm of the degree, and the logarithm of the field size.

Significance. If the counterexample is valid and the reduction to the black-box interpolator incurs only quasi-linear overhead, the result would supply the first output-sensitive quasi-linear bit-complexity algorithm for sparse polynomial multiplication over the integers, directly addressing the open challenge stated in the abstract.

major comments (2)

[Abstract] Abstract (paragraph stating the counterexample): the manuscript asserts that a counterexample to the previously claimed solution is provided, yet neither the counterexample itself nor any verification or proof of its validity appears in the text, rendering the claim unverifiable from the given material.
[Abstract] Abstract (paragraph describing the integer-coefficient algorithm): the claim that employing the existing quasi-linear modular-black-box interpolation algorithm yields quasi-linear bit complexity is load-bearing for the central result, but the text supplies no explicit complexity recurrence, bound on the number of black-box calls, cost of modular reductions, or analysis of lifting steps to confirm that these contribute at most quasi-linear factors.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments. We address each major comment below.

read point-by-point responses

Referee: [Abstract] Abstract (paragraph stating the counterexample): the manuscript asserts that a counterexample to the previously claimed solution is provided, yet neither the counterexample itself nor any verification or proof of its validity appears in the text, rendering the claim unverifiable from the given material.

Authors: We agree that the counterexample and its verification are not present in the manuscript text. In the revised version we will include the explicit counterexample together with a proof of its validity. revision: yes
Referee: [Abstract] Abstract (paragraph describing the integer-coefficient algorithm): the claim that employing the existing quasi-linear modular-black-box interpolation algorithm yields quasi-linear bit complexity is load-bearing for the central result, but the text supplies no explicit complexity recurrence, bound on the number of black-box calls, cost of modular reductions, or analysis of lifting steps to confirm that these contribute at most quasi-linear factors.

Authors: We agree that an explicit complexity analysis is required. The revised manuscript will contain the complexity recurrence, bounds on the number of black-box calls, costs of the modular reductions, and analysis of the lifting steps demonstrating that the overhead remains quasi-linear. revision: yes

Circularity Check

0 steps flagged

No significant circularity; result is direct application of external black-box algorithm.

full rationale

The paper's central claim is that an algorithm with quasi-linear bit complexity for integer-coefficient sparse multiplication is obtained by employing an existing quasi-linear modular-black-box interpolation algorithm. The abstract presents this explicitly as an application of a pre-existing result without deriving the complexity bound from any fitted parameters, self-definitions, or load-bearing self-citations within the paper. The mention of a counterexample to a prior claim is separate and does not create a reduction. No equations or steps in the provided text reduce the claimed complexity to the paper's own inputs by construction. This qualifies as a self-contained application of independent external work.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no explicit free parameters, axioms, or invented entities; the result is framed as a reduction to an existing algorithm whose properties are taken as given.

pith-pipeline@v0.9.1-grok · 5641 in / 1034 out tokens · 19627 ms · 2026-06-27T07:45:35.338889+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

22 extracted references · 11 canonical work pages

[1]

Primes is in p.Annals of Mathematics, 160(2): 781–793, 2004

Manindra Agrawal, Neeraj Kayal, and Nitin Saxena. Primes is in p.Annals of Mathematics, 160(2): 781–793, 2004. ISSN 0003486X. URLhttp://www.jstor.org/stable/3597229

arXiv 2004
[2]

University of Waterloo, 2016

Andrew Arnold.Sparse Polynomial Interpolation and Testing (PhD Thesis). University of Waterloo, 2016

2016
[3]

Cantor and Erich Kaltofen

David G. Cantor and Erich Kaltofen. On fast multiplication of polynomials over arbitrary algebras. Acta Inf., 28(7):693–701, October 1991. ISSN 0001-5903. doi: 10.1007/BF01178683. URLhttps://doi. org/10.1007/BF01178683

work page doi:10.1007/bf01178683 1991
[4]

Verifying candidate matches in sparse and wildcard match- ing

Richard Cole and Ramesh Hariharan. Verifying candidate matches in sparse and wildcard match- ing. InProceedings of the Thiry-Fourth Annual ACM Symposium on Theory of Computing, STOC ’02, pp. 592–601, New York, NY, USA, 2002. Association for Computing Machinery. ISBN 1581134959. doi: 10.1145/509907.509992. URLhttps://doi.org/10.1145/509907.509992

work page doi:10.1145/509907.509992 2002
[5]

Cook and Stål O

Stephen A. Cook and Stål O. Aanderaa. On the minimum computation time of functions.Transactions of the American Mathematical Society, 142:291–314, 1969. ISSN 00029947. URLhttp://www.jstor.org/ stable/1995359

arXiv 1969
[6]

The sparsity challenges

James Harold Davenport and Jacques Carette. The sparsity challenges. In2009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 3–7, 2009. doi: 10.1109/ SYNASC.2009.62. 12 Key Laboratory of Mathematics Mechanization MechMath Agent Team

2009
[7]

Sumsets, 3sum, subset sum: Now for real! InProceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp

Nick Fischer. Sumsets, 3sum, subset sum: Now for real! InProceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 4520–4546, 2025. doi: 10.1137/1.9781611978322.155. URLhttps://epubs.siam.org/doi/abs/10.1137/1.9781611978322.155

work page doi:10.1137/1.9781611978322.155 2025
[8]

Essentially optimal sparse polynomial mul- tiplication

Pascal Giorgi, Bruno Grenet, and Armelle Perret du Cray. Essentially optimal sparse polynomial mul- tiplication. InProceedings of the 45th International Symposium on Symbolic and Algebraic Computation, ISSAC ’20, pp. 202–209, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450371001. doi: 10.1145/3373207.3404026. URLhttps://doi.org/...

work page doi:10.1145/3373207.3404026 2020
[9]

On exact division and divisibility testing for sparse polynomials

Pascal Giorgi, Bruno Grenet, and Armelle Perret du Cray. On exact division and divisibility testing for sparse polynomials. InProceedings of the 2021 International Symposium on Symbolic and Algebraic Compu- tation, ISSAC ’21, pp. 163–170, New York, NY, USA, 2021. Association for Computing Machinery. ISBN 9781450383820. doi: 10.1145/3452143.3465539. URLhtt...

work page doi:10.1145/3452143.3465539 2021
[10]

Pascal Giorgi, Bruno Grenet, Armelle Perret du Cray, and Daniel S. Roche. Sparse polynomial in- terpolation and division in soft-linear time. InProceedings of the 2022 International Symposium on Symbolic and Algebraic Computation, ISSAC ’22, pp. 459–468, New York, NY, USA, 2022. Associa- tion for Computing Machinery. ISBN 9781450386883. doi: 10.1145/34764...

work page doi:10.1145/3476446.3536173 2022
[11]

Polynomial modular product verifica- tion and its implications.Journal of Symbolic Computation, 116:98–129, 2023

Pascal Giorgi, Bruno Grenet, and Armelle Perret du Cray. Polynomial modular product verifica- tion and its implications.Journal of Symbolic Computation, 116:98–129, 2023. ISSN 0747-7171. doi: https://doi.org/10.1016/j.jsc.2022.08.011. URLhttps://www.sciencedirect.com/science/article/ pii/S0747717122000773

work page doi:10.1016/j.jsc.2022.08.011 2023
[12]

Fast polynomial computations with space constraints, 2026

Bruno Grenet. Fast polynomial computations with space constraints, 2026. URLhttps://arxiv.org/ abs/2511.11267

arXiv 2026
[13]

G. H. Hardy and E. M. Wright.An Introduction to the Theory of Numbers. Oxford University Press, 6th edition, 2008

2008
[14]

Sparse polynomial interpolation over fields with large or zero characteristic

Qiao-Long Huang. Sparse polynomial interpolation over fields with large or zero characteristic. In Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation, ISSAC ’19, pp. 219–226, New York, NY, USA, 2019. Association for Computing Machinery. ISBN 9781450360845. doi: 10.1145/3326229.3326250. URLhttps://doi.org/10.1145/3326229.3326250

work page doi:10.1145/3326229.3326250 2019
[15]

Shaving logs via large sieve inequality: Faster algorithms for sparse convolu- tion and more

Ce Jin and Yinzhan Xu. Shaving logs via large sieve inequality: Faster algorithms for sparse convolu- tion and more. InProceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, pp. 1573–1584, New York, NY, USA, 2024. Association for Computing Machinery. ISBN 9798400703836. doi: 10.1145/3618260.3649605. URLhttps://doi.org/10.1145/3618...

work page doi:10.1145/3618260.3649605 2024
[16]

Multiplication of many-digital numbers by auto- matic computers

Anatolii Alekseevich Karatsuba and Yu P Ofman. Multiplication of many-digital numbers by auto- matic computers. InDoklady Akademii Nauk, volume 145, pp. 293–294. Russian Academy of Sciences, 1962

1962
[17]

Mechmath agent team

MechMath Team. Mechmath agent team. Academy of Mathematics and Systems Science, Chinese Academy of Sciences, 2026. URLhttps://eonmath.github.io/mechmath

2026
[18]

Nearly optimal sparse polynomial multiplication.IEEE Transactions on Information Theory, 66(11):7231–7236, 2020

Vasileios Nakos. Nearly optimal sparse polynomial multiplication.IEEE Transactions on Information Theory, 66(11):7231–7236, 2020

2020
[19]

Daniel S. Roche. What can (and can’t) we do with sparse polynomials? InProceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC ’18, pp. 25–30, New York, NY, USA, 2018. Association for Computing Machinery. ISBN 9781450355506. doi: 10.1145/3208976. 3209027. URLhttps://doi.org/10.1145/3208976.3209027

work page doi:10.1145/3208976 2018
[20]

and Strassen, V

A. Schönhage and V . Strassen. Schnelle multiplikation großer zahlen.Computing, 7(3):281–292, 1971. ISSN 1436-5057. doi: 10.1007/BF02242355. URLhttps://doi.org/10.1007/BF02242355

work page doi:10.1007/bf02242355 1971
[21]

A. L. Toom. The complexity of a scheme of functional elements realizing the multiplication of integers. Soviet Mathematics Doklady, 3:714–716, 1963

1963
[22]

Cambridge University Press, 2013

Joachim von zur Gathen and Jürgen Gerhard.Modern Computer Algebra. Cambridge University Press, 2013. 13 Key Laboratory of Mathematics Mechanization MechMath Agent Team A Lean Formalization Details This appendix summarizes Lean development at the level of mathematical structure rather than source code. Ordinary algebraic, combinatorial, and cost-envelope o...

2013

[1] [1]

Primes is in p.Annals of Mathematics, 160(2): 781–793, 2004

Manindra Agrawal, Neeraj Kayal, and Nitin Saxena. Primes is in p.Annals of Mathematics, 160(2): 781–793, 2004. ISSN 0003486X. URLhttp://www.jstor.org/stable/3597229

arXiv 2004

[2] [2]

University of Waterloo, 2016

Andrew Arnold.Sparse Polynomial Interpolation and Testing (PhD Thesis). University of Waterloo, 2016

2016

[3] [3]

Cantor and Erich Kaltofen

David G. Cantor and Erich Kaltofen. On fast multiplication of polynomials over arbitrary algebras. Acta Inf., 28(7):693–701, October 1991. ISSN 0001-5903. doi: 10.1007/BF01178683. URLhttps://doi. org/10.1007/BF01178683

work page doi:10.1007/bf01178683 1991

[4] [4]

Verifying candidate matches in sparse and wildcard match- ing

Richard Cole and Ramesh Hariharan. Verifying candidate matches in sparse and wildcard match- ing. InProceedings of the Thiry-Fourth Annual ACM Symposium on Theory of Computing, STOC ’02, pp. 592–601, New York, NY, USA, 2002. Association for Computing Machinery. ISBN 1581134959. doi: 10.1145/509907.509992. URLhttps://doi.org/10.1145/509907.509992

work page doi:10.1145/509907.509992 2002

[5] [5]

Cook and Stål O

Stephen A. Cook and Stål O. Aanderaa. On the minimum computation time of functions.Transactions of the American Mathematical Society, 142:291–314, 1969. ISSN 00029947. URLhttp://www.jstor.org/ stable/1995359

arXiv 1969

[6] [6]

The sparsity challenges

James Harold Davenport and Jacques Carette. The sparsity challenges. In2009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 3–7, 2009. doi: 10.1109/ SYNASC.2009.62. 12 Key Laboratory of Mathematics Mechanization MechMath Agent Team

2009

[7] [7]

Sumsets, 3sum, subset sum: Now for real! InProceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp

Nick Fischer. Sumsets, 3sum, subset sum: Now for real! InProceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 4520–4546, 2025. doi: 10.1137/1.9781611978322.155. URLhttps://epubs.siam.org/doi/abs/10.1137/1.9781611978322.155

work page doi:10.1137/1.9781611978322.155 2025

[8] [8]

Essentially optimal sparse polynomial mul- tiplication

Pascal Giorgi, Bruno Grenet, and Armelle Perret du Cray. Essentially optimal sparse polynomial mul- tiplication. InProceedings of the 45th International Symposium on Symbolic and Algebraic Computation, ISSAC ’20, pp. 202–209, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450371001. doi: 10.1145/3373207.3404026. URLhttps://doi.org/...

work page doi:10.1145/3373207.3404026 2020

[9] [9]

On exact division and divisibility testing for sparse polynomials

Pascal Giorgi, Bruno Grenet, and Armelle Perret du Cray. On exact division and divisibility testing for sparse polynomials. InProceedings of the 2021 International Symposium on Symbolic and Algebraic Compu- tation, ISSAC ’21, pp. 163–170, New York, NY, USA, 2021. Association for Computing Machinery. ISBN 9781450383820. doi: 10.1145/3452143.3465539. URLhtt...

work page doi:10.1145/3452143.3465539 2021

[10] [10]

Pascal Giorgi, Bruno Grenet, Armelle Perret du Cray, and Daniel S. Roche. Sparse polynomial in- terpolation and division in soft-linear time. InProceedings of the 2022 International Symposium on Symbolic and Algebraic Computation, ISSAC ’22, pp. 459–468, New York, NY, USA, 2022. Associa- tion for Computing Machinery. ISBN 9781450386883. doi: 10.1145/34764...

work page doi:10.1145/3476446.3536173 2022

[11] [11]

Polynomial modular product verifica- tion and its implications.Journal of Symbolic Computation, 116:98–129, 2023

Pascal Giorgi, Bruno Grenet, and Armelle Perret du Cray. Polynomial modular product verifica- tion and its implications.Journal of Symbolic Computation, 116:98–129, 2023. ISSN 0747-7171. doi: https://doi.org/10.1016/j.jsc.2022.08.011. URLhttps://www.sciencedirect.com/science/article/ pii/S0747717122000773

work page doi:10.1016/j.jsc.2022.08.011 2023

[12] [12]

Fast polynomial computations with space constraints, 2026

Bruno Grenet. Fast polynomial computations with space constraints, 2026. URLhttps://arxiv.org/ abs/2511.11267

arXiv 2026

[13] [13]

G. H. Hardy and E. M. Wright.An Introduction to the Theory of Numbers. Oxford University Press, 6th edition, 2008

2008

[14] [14]

Sparse polynomial interpolation over fields with large or zero characteristic

Qiao-Long Huang. Sparse polynomial interpolation over fields with large or zero characteristic. In Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation, ISSAC ’19, pp. 219–226, New York, NY, USA, 2019. Association for Computing Machinery. ISBN 9781450360845. doi: 10.1145/3326229.3326250. URLhttps://doi.org/10.1145/3326229.3326250

work page doi:10.1145/3326229.3326250 2019

[15] [15]

Shaving logs via large sieve inequality: Faster algorithms for sparse convolu- tion and more

Ce Jin and Yinzhan Xu. Shaving logs via large sieve inequality: Faster algorithms for sparse convolu- tion and more. InProceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, pp. 1573–1584, New York, NY, USA, 2024. Association for Computing Machinery. ISBN 9798400703836. doi: 10.1145/3618260.3649605. URLhttps://doi.org/10.1145/3618...

work page doi:10.1145/3618260.3649605 2024

[16] [16]

Multiplication of many-digital numbers by auto- matic computers

Anatolii Alekseevich Karatsuba and Yu P Ofman. Multiplication of many-digital numbers by auto- matic computers. InDoklady Akademii Nauk, volume 145, pp. 293–294. Russian Academy of Sciences, 1962

1962

[17] [17]

Mechmath agent team

MechMath Team. Mechmath agent team. Academy of Mathematics and Systems Science, Chinese Academy of Sciences, 2026. URLhttps://eonmath.github.io/mechmath

2026

[18] [18]

Nearly optimal sparse polynomial multiplication.IEEE Transactions on Information Theory, 66(11):7231–7236, 2020

Vasileios Nakos. Nearly optimal sparse polynomial multiplication.IEEE Transactions on Information Theory, 66(11):7231–7236, 2020

2020

[19] [19]

Daniel S. Roche. What can (and can’t) we do with sparse polynomials? InProceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC ’18, pp. 25–30, New York, NY, USA, 2018. Association for Computing Machinery. ISBN 9781450355506. doi: 10.1145/3208976. 3209027. URLhttps://doi.org/10.1145/3208976.3209027

work page doi:10.1145/3208976 2018

[20] [20]

and Strassen, V

A. Schönhage and V . Strassen. Schnelle multiplikation großer zahlen.Computing, 7(3):281–292, 1971. ISSN 1436-5057. doi: 10.1007/BF02242355. URLhttps://doi.org/10.1007/BF02242355

work page doi:10.1007/bf02242355 1971

[21] [21]

A. L. Toom. The complexity of a scheme of functional elements realizing the multiplication of integers. Soviet Mathematics Doklady, 3:714–716, 1963

1963

[22] [22]

Cambridge University Press, 2013

Joachim von zur Gathen and Jürgen Gerhard.Modern Computer Algebra. Cambridge University Press, 2013. 13 Key Laboratory of Mathematics Mechanization MechMath Agent Team A Lean Formalization Details This appendix summarizes Lean development at the level of mathematical structure rather than source code. Ordinary algebraic, combinatorial, and cost-envelope o...

2013