Keypoint Detector Math

SIFT, SURF, ORB, BRISK and AKAZE all run the same six steps. They differ in the scale space, the response, the orientation and the descriptor. The constants below are OpenCV 4.12 defaults, checked against its source code.

Shared pipeline

Every detector here runs these six steps in this order.

  1. Build a scale space, so each feature is found at its own size.
  2. Compute a response at every pixel and every scale.
  3. Keep the local maxima above a threshold (SIFT keeps minima too), and refine their position.
  4. Assign an orientation, so the descriptor turns with the feature.
  5. Sample a patch in the keypoint's frame (position, scale, angle) and encode it.
  6. Compare descriptors with a distance: L2 for float vectors, Hamming for bit strings.

Notation used in every section:

  • I(x, y) is the grayscale image. Ix and Iy are its derivatives, computed as finite differences.
  • L(x, y, σ) is the image blurred by a Gaussian of scale σ. Lx, Lxx and Lxy are derivatives of L.
  • s is the keypoint's scale, in pixels of the original image.
G(x,y,σ)=12πσ2exp⁡(−x2+y22σ2),G(x,y,\sigma) = \frac{1}{2\pi\sigma^2}\exp\left(-\frac{x^2+y^2}{2\sigma^2}\right),L(x,y,σ)=G(x,y,σ)∗I(x,y)L(x,y,\sigma) = G(x,y,\sigma) * I(x,y)

Scale normalization multiplies an n-th derivative by σⁿ. Responses at different scales then compare fairly. The scale where the response peaks is the feature's size.

dL2(a,b)=∥a−b∥2,d_{L2}(a,b) = \lVert a-b \rVert_2,dH(a,b)=popcount⁡(a⊕b)d_{H}(a,b) = \operatorname{popcount}(a \oplus b)

SIFT

SIFT finds blobs as extrema of a Difference-of-Gaussians (DoG) pyramid. It describes each blob with 128 gradient-histogram values. The math from the scale space to the normalization is checked in Lean 4 and Mathlib, for exact real numbers (proofs). Float rounding is not covered, and each proof file lists what else it leaves out.

Scale space. Each octave halves the image. Inside an octave, σ grows by k = 2^(1/S), with S = 3 layers (nOctaveLayers), so σ doubles after S layers. OpenCV blurs each layer from the one before by √(σᵢ₊₁² − σᵢ²). Blurs add in variance, so layer i has exactly σᵢ = σ₀kⁱ. Halving layer S then starts the next octave at exactly σ₀ = 1.6. OpenCV assumes the input already has a blur of 0.5. It doubles the image first, so that blur becomes 1, then adds √(σ₀² − 1). That gives exactly σ₀ only if the upscale adds no blur. OpenCV's bilinear upscale adds some, so the real base blur is about 1.82.

Response. The DoG is the difference of two neighboring blur levels:

D(x,y,σ)=L(x,y,kσ)−L(x,y,σ)≈(k−1) σ2∇2G∗ID(x,y,\sigma) = L(x,y,k\sigma) - L(x,y,\sigma) \approx (k-1)\,\sigma^2\nabla^2 G * I

The approximation follows from the heat equation ∂G/∂σ = σ∇²G: as k → 1, (G(kσ) − G(σ))/(k − 1) tends to σ²∇²G. OpenCV's k = 2^(1/3) ≈ 1.26 is a fixed step, so it only approximates that limit. So the DoG is close to a scale-normalized Laplacian of Gaussian, at the cost of one subtraction per pixel. The DoG kernel G(kσ) − G(σ) is lowest, and negative, at its center. A bright point is therefore a DoG minimum, and a dark point a maximum.

Extrema. A sample is a candidate if it is positive and ≥ all 26 neighbors, or negative and ≤ all of them. Ties pass. The neighbors are 8 at its own scale, 9 above and 9 below. OpenCV first skips samples with |D| ≤ ⌊0.5 × contrastThreshold / S × 255⌋ / 255. That is 1/255 by default, at most half the final contrast threshold.

Sub-pixel fit. A second-order Taylor expansion in x = (x, y, σ) locates the true extremum:

D(x)≈D+∇D⊤x+12 x⊤H x,D(\mathbf{x}) \approx D + \nabla D^{\top}\mathbf{x} + \tfrac{1}{2}\,\mathbf{x}^{\top}H\,\mathbf{x},x^=−H−1∇D\hat{\mathbf{x}} = -H^{-1}\nabla D

x̂ is the model's only stationary point when H is invertible. It is a minimum when H is positive definite, and a maximum when H is negative definite. OpenCV checks neither, so a kept point can be a saddle of the model. If any offset is 0.5 or more, OpenCV moves the sample by the rounded offset and fits again. It fits at most 5 times in all. It drops the point if the fit never settles, leaves the layers, or comes within 5 pixels of the border.

Contrast test. The refined value is the model's value at x̂, D(x̂) = D + ½∇Dᵀx̂. Lowe rejects |D(x̂)| < 0.03 for pixel values in [0, 1]. OpenCV rejects |D(x̂)| × S < contrastThreshold (0.04). That is a threshold of 0.04/3 = 1/75 ≈ 0.0133 on |D(x̂)|, less than half of Lowe's. Setting contrastThreshold = 0.09 gives Lowe's test.

Edge test. On an edge the DoG is strong, but the position along the edge is uncertain. Let r ≥ 1 be the ratio of the two eigenvalues of the 2×2 Hessian of D, larger over smaller by magnitude:

Tr⁡(H)2Det⁡(H)=(r+1)2r  <  (rmax⁡+1)2rmax⁡,\frac{\operatorname{Tr}(H)^2}{\operatorname{Det}(H)} = \frac{(r+1)^2}{r} \;<\; \frac{(r_{\max}+1)^2}{r_{\max}},rmax⁡=10r_{\max} = 10

(r + 1)²/r grows with r for r ≥ 1, so the test says exactly r < r_max. A point that fails it is dropped. Det(H) < 0 means a saddle, with eigenvalues of opposite sign. Det(H) = 0 means a zero eigenvalue. OpenCV drops both, and calls r_max edgeThreshold.

Orientation. Gradient magnitude and angle are taken at the keypoint's scale:

m=Lx2+Ly2,m = \sqrt{L_x^2 + L_y^2},θ=atan2⁡(Ly,Lx)\theta = \operatorname{atan2}(L_y, L_x)

A 36-bin histogram of θ (10° per bin) is weighted by m and by a Gaussian with σ = 1.5s, within a radius of 3σ. OpenCV smooths it with a circular [1 4 6 4 1]/16 filter. Every bin above both neighbors and at or above 80% of the maximum adds a keypoint. A parabola through that bin's value c and its neighbors' values l and r refines the peak by t = ½(l − r)/(l − 2c + r) bins. That offset is the parabola's maximum, and it is always within half a bin. A top bin that ties a neighbor adds no keypoint.

Descriptor. A 4×4 grid of cells is laid over the patch, rotated by θ. Each cell is 3s wide in OpenCV. Each cell holds an 8-bin histogram of gradient angle relative to θ, so the descriptor has 4 × 4 × 8 = 128 values. Trilinear interpolation spreads every sample over its 8 neighboring (row, column, angle) bins. The 8 weights are ≥ 0 and sum to 1. OpenCV samples up to half a cell past the grid's edge. It drops the shares that fall outside the 4×4 cells, about a quarter of the weight for a uniform gradient.

Normalization. The vector is scaled to unit length, which cancels a contrast change I → a·I (a > 0). A brightness offset I + b already cancels in the gradients. Entries are then clipped at 0.2, and the vector is normalized again. This limits the effect of saturation and uneven light. OpenCV gets the same vector with one clip, at 0.2 times the raw vector's length. The second normalization can push entries back above 0.2. OpenCV then stores round(512 × entry), capped at 255. The keypoints themselves can still change with contrast, because the contrast test sees the gain.

Distance. L2. Lowe's ratio test keeps a match when d₁/d₂ < 0.8.

SIFT reads a 4 × 4 grid of cells, turned to the keypoint’s orientationEach cell is an 8-bin histogram of gradient angle: 4 × 4 × 8 = 128 valuesθOrientation θ, from the angle histogramThe whole grid turns with θOne cell is 3s wide in OpenCVs = the keypoint’s scale8 spokes = 8 bins of gradient angleEach angle is measured from θGaussian weight on every sampleσ = half the window widthTrilinear interpolationEach sample is shared between neighboringcells and neighboring angle binsNormalize, clip at 0.2, normalizeCancels contrast and limits saturation
SIFT descriptor · 4 × 4 cells × 8 angle bins

The grid turns with θ, so a rotated copy of the patch gives the same 128 values.

SURF

SURF finds blobs with a box-filter approximation of the Hessian determinant. It describes each blob with 64 sums of Haar-wavelet responses.

Integral image. The sum over any rectangle costs 4 lookups, whatever its size:

S(x,y)=∑i≤x∑j≤yI(i,j),S(x,y) = \sum_{i \le x}\sum_{j \le y} I(i,j),∑rectI=S(D)−S(B)−S(C)+S(A)\sum_{\text{rect}} I = S(D) - S(B) - S(C) + S(A)

A, B, C and D are the rectangle's corners, from top-left to bottom-right.

Response. The Hessian determinant is large at blobs. SURF replaces the Gaussian second derivatives with box filters Dxx, Dyy and Dxy, each divided by its area:

det⁡H≈DxxDyy−(0.9 Dxy)2\det H \approx D_{xx}D_{yy} - (0.9\,D_{xy})^2

A 9×9 box filter approximates σ = 1.2. The weight 0.9 corrects the mismatch between box filters and true Gaussians. OpenCV writes it as dx · dy − 0.81 · dxy².

Scale space. The image never shrinks; the filter grows instead. OpenCV uses size = (9 + 6 × layer) × 2^octave, and the scale is s = 1.2 × size / 9.

Detection. The determinant is thresholded (hessianThreshold: 100 by default, 400 in the bench script). Maxima are kept in a 3×3×3 neighborhood. They are refined with the same quadratic fit as SIFT.

Orientation. Haar wavelet responses (dx, dy) of size 4s are sampled within radius 6s. They are weighted by a Gaussian: 2s in the 2008 paper, 2.5s in OpenCV. A 60° sector slides around the circle, and the response vectors inside it are summed. The longest sum gives the orientation.

Descriptor. A square of side 20s is rotated to the orientation and split into 4×4 subregions of 5×5 samples. Haar responses of size 2s are weighted by a Gaussian of σ = 3.3s. Each subregion contributes four values:

v=(∑dx, ∑dy, ∑∣dx∣, ∑∣dy∣)v = \left(\sum d_x,\ \sum d_y,\ \sum |d_x|,\ \sum |d_y|\right)

That gives 16 × 4 = 64 values, normalized to unit length. The extended version splits each sum by sign and gives 128 values.

Laplacian sign. The sign of Lxx + Lyy tells a bright blob on a dark ground from the reverse. A matcher can skip pairs whose signs differ.

Distance. L2.

SURF orients with a sliding 60° sector, then sums Haar responses in a 4 × 4 gridDistances in units of the keypoint scale sOrientationHaar responses (size 4s) at 113 points within 6sA 60° sector slides around the circle; its responses add upThe longest summed vector sets the orientationDescriptorA 20s square turned to the orientation4 × 4 subregions × 5 × 5 samples, Haar size 2sHighlighted subregion: Σdx, Σdy, Σ|dx|, Σ|dy|16 subregions × 4 sums = 64 values
SURF · 60° orientation sector and 4 × 4 descriptor grid

The sector finds the dominant gradient direction. The descriptor square is then turned to that direction before the sums are taken.

ORB

ORB finds FAST corners on a pyramid and orients them by their intensity centroid. It describes each corner with 256 learned pixel comparisons.

Pyramid. 8 levels, each 1/1.2 the size of the level before (nlevels, scaleFactor). Detection runs on every level.

FAST. The 16 pixels on a circle of radius 3 around p are tested. p is a corner when 9 contiguous circle pixels are all brighter than I(p) + t, or all darker than I(p) − t. OpenCV's fastThreshold sets t = 20.

Harris ranking. FAST has no reliable strength measure and also fires on edges. ORB ranks the candidates with the Harris score of the structure tensor M:

M=∑window[Ix2IxIyIxIyIy2],M = \sum_{\text{window}} \begin{bmatrix} I_x^2 & I_xI_y \\ I_xI_y & I_y^2 \end{bmatrix},R=det⁡M−0.04 (tr⁡M)2R = \det M - 0.04\,(\operatorname{tr} M)^2

The best nfeatures candidates by R are kept.

Orientation. Moments are taken over a disk of radius 15 px centered on the keypoint:

mpq=∑x,yxp yq I(x,y),m_{pq} = \sum_{x,y} x^p\,y^q\,I(x,y),θ=atan2⁡(m01, m10)\theta = \operatorname{atan2}(m_{01},\ m_{10})

θ points from the corner to its intensity centroid (m10/m00, m01/m00).

Bit tests. Each level is first smoothed with a 7×7 Gaussian of σ = 2. One test compares two points, and 256 tests form the descriptor:

τ(a,b)={1I(a)<I(b)0otherwise,\tau(a,b) = \begin{cases} 1 & I(a) < I(b) \\ 0 & \text{otherwise} \end{cases},f=∑i=12562 i−1 τ(ai,bi)f = \sum_{i=1}^{256} 2^{\,i-1}\,\tau(a_i, b_i)

Steering. The 512 test points are rotated by θ, so the descriptor turns with the feature: Sθ = Rθ · S. The paper rounds θ to 12° steps and precomputes 30 rotated patterns. OpenCV rotates each test point by the exact angle instead.

Learned pairs. Rotated tests become correlated and carry less information. ORB therefore chose its 256 pairs from about 205,000 candidates in a 31×31 patch. A greedy search kept tests with a mean near 0.5 and low correlation with the tests already kept. OpenCV stores the result as a fixed table.

Distance. Hamming. With WTA_K = 3 or 4, each test compares 3 or 4 points, and the distance is Hamming2.

ORB tests 16 circle pixels for a corner, then compares 256 learned point pairsLeft: the FAST test around pixel p. Right: OpenCV’s rBRIEF table, drawn to scalepFASTCorner: 9 contiguous circle pixels, all brighterthan I(p) + t or all darker than I(p) − tShaded: one passing run. Bold: checked firstrBRIEF test pairs256 lines in a 31 × 31 patch; each compares two smoothed pixelsBold: the first 8 pairs. Dashed: the radius-15 centroid diskOpenCV turns the whole pattern by the exact angle θ
ORB · FAST circle and OpenCV's 256 rBRIEF test pairs

The pairs are OpenCV's bit_pattern_31_ table, drawn to scale. ORB rotates them by θ before it runs the tests.

BRISK

BRISK finds FAST-score maxima across octaves. It describes each keypoint with 512 brightness comparisons on a fixed ring pattern.

Scale space. Octaves cᵢ halve the image. Intra-octaves dᵢ sit between them; d₀ is the image downsampled by 1.5. Their scales are t = 2^i and t = 1.5 × 2^i.

Detection. The FAST test runs on every layer; BRISK uses AGAST, a faster decision tree for the same test. The score s is the largest threshold at which the point is still a corner.

Scale maxima. s must beat its 8 neighbors in its own layer. It must also beat the scores in the layers above and below.

Refinement. A 2D quadratic is fitted to the 3×3 scores in each of the three layers. A parabola along the scale axis through the three peaks gives a continuous position and scale.

Pattern. 60 points sit on 4 rings around a center point, and the pattern scales with t. Each point is blurred by a Gaussian sized to the spacing on its ring, which prevents aliasing:

σk=1.3 rksin⁡ ⁣(πnk)\sigma_k = 1.3\, r_k \sin\!\left(\frac{\pi}{n_k}\right)

Here rₖ is the ring radius and nₖ its point count. OpenCV's radii are 0.85 × (2.9, 4.9, 7.4, 10.8) with 10, 14, 15 and 20 points.

Pairs. The 60 points form 1,770 pairs. In OpenCV, 512 are short (closer than 5.85t) and 870 are long (farther than 8.2t). The other 388 are not used. The paper gives the limits as 9.75t and 13.67t, in other units.

Orientation. Each pair gives a local gradient. The long pairs are averaged:

g(pi,pj)=(pj−pi) I(pj,σj)−I(pi,σi)∥pj−pi∥2,g(p_i,p_j) = (p_j - p_i)\,\frac{I(p_j,\sigma_j) - I(p_i,\sigma_i)}{\lVert p_j - p_i \rVert^2},α=atan2⁡(∑Lgy, ∑Lgx)\alpha = \operatorname{atan2}\Big(\sum_{\mathcal{L}} g_y,\ \sum_{\mathcal{L}} g_x\Big)

Long baselines average out local texture, so they give a stable direction.

Descriptor. The pattern is rotated by α. Each short pair gives one bit, so the 512 short pairs give 512 bits:

b={1I(pjα,σj)>I(piα,σi)0otherwiseb = \begin{cases} 1 & I(p_j^{\alpha}, \sigma_j) > I(p_i^{\alpha}, \sigma_i) \\ 0 & \text{otherwise} \end{cases}

Distance. Hamming.

BRISK samples 60 points on rings and splits their 1,770 pairs by lengthOpenCV’s default pattern at scale t = 1. Circles show each point’s Gaussian blur radius σ512 short pairs, closer than 5.85tEach compares two blurred points: 1 bit512 pairs give the 512-bit descriptor870 long pairs, farther than 8.2tTheir averaged gradients set the orientation αThe other 388 pairs, in between, are unused
BRISK · 60-point pattern, 512 short and 870 long pairs

Short pairs make the bits. Long pairs set the orientation. Both are computed here from OpenCV's ring radii and distance limits.

AKAZE

AKAZE finds Hessian blobs in an edge-preserving nonlinear scale space. It describes each blob with 486 binary comparisons of cell averages.

Why nonlinear. Gaussian blur smooths across edges, so boundaries blur and move at coarse scales. Nonlinear diffusion smooths inside regions and stops at strong edges.

Diffusion. The conductance c falls toward 0 where the smoothed gradient is large, so diffusion stops at edges:

∂L∂t=div⁡(c(x,y,t) ∇L),\frac{\partial L}{\partial t} = \operatorname{div}\big(c(x,y,t)\,\nabla L\big),c=11+∣∇Lσ∣2/λ2c = \frac{1}{1 + |\nabla L_\sigma|^2/\lambda^2}

This is Perona–Malik g2, the OpenCV default. Lσ is a Gaussian-smoothed copy of L. The contrast factor λ is the 70th percentile of the gradient-magnitude histogram, and OpenCV multiplies it by 0.75 at each new octave.

Levels. σᵢ = 1.6 × 2^(o + s/4), over 4 octaves o with 4 sublevels s each. A Gaussian blur of σ equals linear diffusion for time σ²/2, so each level runs to time tᵢ = σᵢ²/2. Each new octave also halves the image.

Fast Explicit Diffusion (FED). An explicit step L ← (Id + τA)L is stable only for τ ≤ 0.25 in 2D. FED runs cycles of n steps with varying sizes:

τj=τmax⁡2cos⁡2 ⁣(π 2j+14n+2),\tau_j = \frac{\tau_{\max}}{2\cos^2\!\left(\pi\,\frac{2j+1}{4n+2}\right)},∑j=0n−1τj=τmax⁡ n2+n3,\sum_{j=0}^{n-1}\tau_j = \tau_{\max}\,\frac{n^2+n}{3},τmax⁡=0.25\tau_{\max} = 0.25

Some single steps exceed 0.25, but each full cycle is stable. One cycle's diffusion time grows with n², where constant steps would grow with n.

Response. The scale-normalized Hessian determinant, with derivatives from 3×3 Scharr filters:

LHessian=σnorm2 (LxxLyy−Lxy2),L_{\text{Hessian}} = \sigma_{\text{norm}}^2\,\big(L_{xx}L_{yy} - L_{xy}^2\big),σnorm=σi/2oi\sigma_{\text{norm}} = \sigma_i / 2^{o_i}

Detection. The threshold is 0.001 (threshold). A point must be a maximum in a 3×3 window and over the levels above and below. A 2D quadratic fit gives the sub-pixel position.

Orientation. As in SURF, but with the derivatives Lx and Ly within radius 6σ and a 60° sliding sector.

Descriptor (M-LDB). The patch is a 20×20 grid of samples spaced σ apart, rotated to the orientation. Grids of 2×2, 3×3 and 4×4 cells divide it, and each cell averages its samples. Each cell gives three values: intensity, Lx and Ly. Every pair of cells in the same grid gives one bit per value:

3[(42)+(92)+(162)]=3 (6+36+120)=486 bits3\left[\binom{4}{2} + \binom{9}{2} + \binom{16}{2}\right] = 3\,(6 + 36 + 120) = 486 \text{ bits}

The 486 bits are stored in 61 bytes.

Distance. Hamming.

M-LDB compares cell averages on three grids: 486 bits per keypointSamples sit σ apart on a grid turned to the keypoint’s orientation. One example pair is shaded per grid2 × 2 grid: 6 pairsCells of 10 × 10 samples3 × 3 grid: 36 pairsCells of 7 × 7 samples4 × 4 grid: 120 pairsCells of 5 × 5 samplesEach cell gives mean intensity, mean Lx and mean Ly, so each pair gives 3 bits3 × (6 + 36 + 120) = 486 bits, stored in 61 bytes
AKAZE M-LDB · 2 × 2, 3 × 3 and 4 × 4 cell grids

OpenCV's 3 × 3 grid uses 7-sample cells, so it reaches one sample row and column past the other two grids.

Matching

The bench page and the Python script match with a ratio test, then fit a homography with RANSAC. The same steps work for all five detectors; only the distance changes.

Ratio test. For each descriptor in A, the two nearest descriptors in B are found, at distances d₁ ≤ d₂. The match is kept when d₁ < 0.75 × d₂. A point with two similar candidates is ambiguous, so it fails.

Homography. H maps a point of image A to image B in homogeneous coordinates:

x′=h11x+h12y+h13h31x+h32y+h33,x' = \frac{h_{11}x + h_{12}y + h_{13}}{h_{31}x + h_{32}y + h_{33}},y′=h21x+h22y+h23h31x+h32y+h33y' = \frac{h_{21}x + h_{22}y + h_{23}}{h_{31}x + h_{32}y + h_{33}}

H has 8 degrees of freedom. Each match gives 2 linear equations, so 4 matches determine H. OpenCV solves them by SVD.

RANSAC. Pick 4 random matches, fit H, and count the matches that H maps to within 3 px. Repeat, keep the H with the most inliers, and refit it on all of them. For confidence p and inlier fraction w, the number of tries is:

N=log⁡(1−p)log⁡(1−w4),N = \frac{\log(1-p)}{\log(1-w^4)},w=0.5, p=0.99  ⇒  N≈72w = 0.5,\ p = 0.99 \;\Rightarrow\; N \approx 72

Corner error. The bench's accuracy measure is the mean distance between H_fit · c and H_true · c over the four image corners c.

Side by side

The float descriptors (SIFT, SURF) use L2; the binary ones (ORB, BRISK, AKAZE) use Hamming.

DetectorScale spaceResponseOrientationDescriptorSizeDistance
SIFTGaussian pyramidDoG ≈ σ²∇²G36-bin gradient histogram4×4 cells × 8 angle bins128 floatsL2
SURFgrowing box filtersHessian determinant from boxesHaar sums in a 60° sector4×4 cells × 4 Haar sums64 floatsL2
ORBpyramid, ×1/1.2 per levelFAST, ranked by Harrisintensity centroid256 learned pixel tests256 bitsHamming
BRISKoctaves + intra-octavesFAST scoremean gradient of long pairs512 short-pair tests on rings512 bitsHamming
AKAZEnonlinear diffusion (FED)scale-normalized Hessianderivative sums in a 60° sectorM-LDB cell comparisons486 bitsHamming

Sources

OpenCV values were read from the 4.12.0 source. Values marked as the paper's come from the original papers, cited from memory and not re-read for this doc.

  • OpenCV 4.12.0 source: sift.simd.hpp, orb.cpp, brisk.cpp, AKAZEFeatures.cpp, AKAZEConfig.h, fed.cpp
  • SIFT proofs in Lean 4 and Mathlib: lean-keypoint-math, checked against OpenCV 4.12.0's sift.dispatch.cpp and sift.simd.hpp
  • opencv_contrib 4.12.0 source: surf.cpp
  • Lowe, Distinctive Image Features from Scale-Invariant Keypoints, IJCV, 2004
  • Bay, Ess, Tuytelaars, Van Gool, Speeded-Up Robust Features (SURF), CVIU, 2008
  • Rublee, Rabaud, Konolige, Bradski, ORB: An efficient alternative to SIFT or SURF, ICCV, 2011
  • Leutenegger, Chli, Siegwart, BRISK: Binary Robust Invariant Scalable Keypoints, ICCV, 2011
  • Alcantarilla, Nuevo, Bartoli, Fast Explicit Diffusion for Accelerated Features in Nonlinear Scale Spaces, BMVC, 2013

Checked in Lean

The math behind OpenCV 4.12's SIFT, checked by Lean 4 and Mathlib.

Theorems
104
Gaps (sorry)
0
Axioms
Lean's standard three
Numbers
Exact reals, no float

What is proved

Each file lists what it does not model. SURF, ORB, BRISK and AKAZE are not started.
Source and build steps on GitHub