Trained Sine Approximator Network

This file contains the weights for a neural network trained to approximate sin(x).

• Architecture: 1 → 8 → 8 → 1 with ReLU activations
• Training domain: x ∈ [0, π]
• Weights exported as exact rational numbers

def LeanCert.Examples.ML.SineApprox.layer1Weights : List (List ℚ)

Layer 1: 1 → 8

Equations

• LeanCert.Examples.ML.SineApprox.layer1Weights = [[1480 / 2361], [-1927 / 9855], [13784 / 8087], [11302 / 7963], [-2570 / 7761], [-2842 / 8583], [15557 / 6552], [-8587 / 8380]]

def LeanCert.Examples.ML.SineApprox.layer1Bias : List ℚ

Equations

• LeanCert.Examples.ML.SineApprox.layer1Bias = [-63 / 1639, 0, 1385 / 3863, -1459 / 4189, 0, 0, 26 / 237, -2971 / 2884]

def LeanCert.Examples.ML.SineApprox.layer2Weights : List (List ℚ)

Layer 2: 8 → 8

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Examples.ML.SineApprox.layer2Bias : List ℚ

Equations

• LeanCert.Examples.ML.SineApprox.layer2Bias = [0, 0, -3035 / 4604, -270 / 4181, 0, -365 / 3467, -33 / 8146, -3727 / 7452]

def LeanCert.Examples.ML.SineApprox.layer3Weights : List (List ℚ)

Layer 3: 8 → 1

Equations

• LeanCert.Examples.ML.SineApprox.layer3Weights = [[-166 / 9267, 7231 / 9243, -11426 / 8859, 3482 / 8621, 209 / 4802, 13014 / 9245, 413 / 9221, 14475 / 8737]]

def LeanCert.Examples.ML.SineApprox.layer3Bias : List ℚ

Equations

• LeanCert.Examples.ML.SineApprox.layer3Bias = [6054 / 9707]

def LeanCert.Examples.ML.SineApprox.layer1 : ML.Layer

Equations

• LeanCert.Examples.ML.SineApprox.layer1 = { weights := LeanCert.Examples.ML.SineApprox.layer1Weights, bias := LeanCert.Examples.ML.SineApprox.layer1Bias }

def LeanCert.Examples.ML.SineApprox.layer2 : ML.Layer

Equations

• LeanCert.Examples.ML.SineApprox.layer2 = { weights := LeanCert.Examples.ML.SineApprox.layer2Weights, bias := LeanCert.Examples.ML.SineApprox.layer2Bias }

def LeanCert.Examples.ML.SineApprox.layer3 : ML.Layer

Equations

• LeanCert.Examples.ML.SineApprox.layer3 = { weights := LeanCert.Examples.ML.SineApprox.layer3Weights, bias := LeanCert.Examples.ML.SineApprox.layer3Bias }