Search research articles

ABOUT JoVE

Overview Leadership Blog JoVE Help Center

AUTHORS

Publishing Process Editorial Board Scope & Policies Peer Review FAQ Submit

LIBRARIANS

Testimonials Subscriptions Access Resources Library Advisory Board FAQ

RESEARCH

JoVE Journal Methods Collections JoVE Encyclopedia of Experiments Archive

EDUCATION

JoVE Core JoVE Business JoVE Science Education JoVE Lab Manual Faculty Resource Center Faculty Site

Terms & Conditions of Use

Related Concept Videos

Fundamental Theorem of Algebra

Fundamental Theorem of Algebra

The Fundamental Theorem of Algebra is central to the study of polynomial equations, asserting that every non-constant polynomial with complex coefficients has at least one complex zero. This means that a polynomial of degree n ≥ 1, written as: with an ≠ 0, has at least one solution in the complex number system. Since the set of real numbers is a subset of complex numbers, this theorem applies equally to polynomials with real coefficients.Building on this result, the...

Block Diagram Reduction

Block Diagram Reduction

The process of deriving the transfer function of a control system often involves reducing its block diagram to a single block. This simplification can be achieved through a series of strategic operations, including relocating branch points and comparators. These operations preserve the overall function of the system while allowing for easier manipulation and combination of blocks.
The first step in this process is the identification and relocation of a branch point. A branch point, where a...

Partial Fractions

Partial Fractions

A partial fraction is a component of a rational expression represented as the sum of simpler fractions. When a rational function is expressed as a ratio of two polynomials, it can often be decomposed into a sum of fractions whose denominators are simpler polynomials, typically linear or irreducible quadratic factors. This process is called partial fraction decomposition, and it is used to simplify complex expressions for integration, solving equations, or analysis.Partial fraction decomposition...

Synthetic Disvision of Polynomials

Synthetic Disvision of Polynomials

Synthetic division is an efficient algorithmic approach for dividing a polynomial by a linear binomial of the form x - c, where c is a real number. This method is helpful due to its streamlined process, which avoids the more cumbersome steps involved in the traditional long division of polynomials. It simplifies computation and serves as a practical tool for evaluating polynomials and identifying their factors.To perform synthetic division, one begins by listing the coefficients of the...

Thevinin's Theorem

Thevinin's Theorem

Thévenin's theorem plays a pivotal role in electrical circuit analysis, offering a solution to the challenges posed by variable loads within a circuit. In practical applications, it is common to encounter circuits where certain elements remain fixed while others fluctuate, often referred to as the "load." A typical household electrical outlet serves as a prime example of a variable load, as it can be connected to a variety of appliances, each with its own unique electrical characteristics.

Theorems of Pappus and Guldinus: Problem Solving

Theorems of Pappus and Guldinus: Problem Solving

Pappus and Guldinus's theorems are powerful mathematical principles that are used for finding the surface area and volume of composite shapes. For example, consider a cylindrical storage tank with a conical top. Finding the surface area or volume can be challenging for such complex shapes. These theorems are particularly useful in calculating the volume and surface area of such systems. Here, the cylindrical storage tank with a conical top can be broken down into two simple shapes: a...

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by

Same author

Intelligent Sensor Software for Robust and Energy-Sustainable Decision-Making in Welding of Steel Reinforcement for Concrete.

Sensors (Basel, Switzerland)·2025

Same author

Analysis of Varroa Mite Colony Infestation Level Using New Open Software Based on Deep Learning Techniques.

Sensors (Basel, Switzerland)·2024

Same author

A Formalization of the Smith Normal Form in Higher-Order Logic.

Journal of automated reasoning·2022

Same author

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm.

Journal of automated reasoning·2020

Same author

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

Journal of automated reasoning·2020

Same author

Relative Termination via Dependency Pairs.

Journal of automated reasoning·2018

Search research articles

Related Experiment Video

Updated: Dec 11, 2025

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Published on: March 18, 2019

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.

René Thiemann¹, Ralph Bottesch¹, Jose Divasón²

¹University of Innsbruck, Innsbruck, Austria.

Journal of Automated Reasoning

|August 25, 2020

Summary

The Lenstra–Lenstra–Lovász (LLL) algorithm provides a polynomial-time solution for finding short lattice vectors, crucial for cryptography and computer algebra. This paper presents a verified implementation of the LLL algorithm and its application in polynomial factorization.

Keywords:

Certified algorithm Complexity verification Lattices Polynomial factorization Shortest vector problem Verified LLL implementation

More Related Videos

Reduction in Left Ventricular Wall Stress and Improvement in Function in Failing Hearts using Algisyl-LVR

Reduction in Left Ventricular Wall Stress and Improvement in Function in Failing Hearts using Algisyl-LVR

Published on: April 8, 2013

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

Related Experiment Videos

Last Updated: Dec 11, 2025

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Generating Strictly Controlled Stimuli for Figure Recognition Experiments

Published on: March 18, 2019

Reduction in Left Ventricular Wall Stress and Improvement in Function in Failing Hearts using Algisyl-LVR

Reduction in Left Ventricular Wall Stress and Improvement in Function in Failing Hearts using Algisyl-LVR

Published on: April 8, 2013

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Generation and Coherent Control of Pulsed Quantum Frequency Combs

Published on: June 8, 2018

Area of Science:

Computational mathematics
Computer science theory
Cryptography

Background:

The Lenstra–Lenstra–Lovász (LLL) algorithm was the first polynomial-time algorithm for lattice basis reduction.
It enables finding short vectors in a lattice, approximating an NP-hard problem.
LLL has significant applications in number theory, computer algebra, and cryptography.

Purpose of the Study:

To provide a verified implementation of the LLL algorithm.
To demonstrate the efficiency and correctness of the implemented LLL algorithm.
To integrate a verified polynomial factorization algorithm using LLL.

Main Methods:

Implementation of the LLL basis reduction algorithm.
Formal verification of the algorithm's soundness and polynomial running-time using Isabelle/HOL.
Integration of LLL with a verified factorization algorithm for univariate integer polynomials.

Main Results:

A practically efficient and formally verified implementation of the LLL algorithm.
The verified implementation achieves performance comparable to commercial systems.
Demonstrated polynomial-time verified factorization of univariate integer polynomials using the LLL algorithm.

Conclusions:

The verified LLL implementation is efficient and reliable for lattice reduction tasks.
Formal verification ensures the correctness of the algorithm and its applications.
The integrated polynomial factorization algorithm offers a verified, polynomial-time solution.