TorchLean
TorchLean is the first unified Lean 4 framework for neural-network specification, execution, and verification.
파일 탐색기
최종 버전 다운로드 (.zip)- blueprint.yml
- ci.yml
- Applications.lean
- Backends.lean
- Foundations.lean
- Numerics.lean
- Runtime.lean
- Verification.lean
- geometry3d-wilddet3d-bbox-diagnostic.png
- torchlean-guide-map.png
- API_Tour.lean
- Motivation.lean
- Overview.lean
- RunningExample.lean
- TheLeanLanguage.lean
- TorchLeanVsPyTorch.lean
- WhyFunctionalProgramming.lean
- AutogradWalkthrough.lean
- BackendSelection.lean
- BuildingModels.lean
- DataAndLoaders.lean
- ExecutionModes.lean
- PyTorchRoundtrip.lean
- RuntimeAndAutograd.lean
- ScientificForwardModels.lean
- TensorsAndShapes.lean
- TorchLeanAPI.lean
- TrainingFromScratch.lean
- ExternalToolsAndFFI.lean
- FloatingPointLiterature.lean
- Floats.lean
- GPUAndCUDA.lean
- GraphsAndIR.lean
- GraphSpec.lean
- SpecLayer.lean
- ApproximationTheory.lean
- AutogradProofs.lean
- Certificates.lean
- ClassicalMLProofs.lean
- FactorizationsCholeskyQR.lean
- FP32Soundness.lean
- LearningTheory.lean
- OptimizationTheory.lean
- ProbabilityAndGradients.lean
- ProofSystems.lean
- RuntimeApproximation.lean
- ScientificMLVerification.lean
- SelfSupervisedTheory.lean
- TwoStageWorkflows.lean
- Verification.lean
- BugZooCatalog.lean
- CLI.lean
- Examples.lean
- GenerativeModels.lean
- ModelZooDeepDive.lean
- ModernModels.lean
- ReinforcementLearning.lean
- Widgets.lean
- Conclusion.lean
- FormalizationMap.lean
- Guide.lean
- lake-manifest.json
- lakefile.toml
- lean-toolchain
- TorchLeanBlueprint.lean
- TorchLeanBlueprintMain.lean
- torchlean_dgemm_cuda.cu
- torchlean_dgemm_cuda_stub.c
- torchlean_cublas_common.h
- torchlean_cuda_buffer.h
- torchlean_cuda_common.h
- torchlean_cuda_deterministic_reductions_env.h
- torchlean_cuda_rng_common.h
- torchlean_size_common.h
- torchlean_cuda_conv_pool.cu
- torchlean_cuda_conv_pool_common.h
- torchlean_cuda_conv_pool_stub.c
- torchlean_cuda_kernels.cu
- torchlean_cuda_kernels_stub.c
- torchlean_libtorch_sdpa.cpp
- torchlean_libtorch_sdpa_stub.c
- torchlean_cuda_tensor.cu
- torchlean_cuda_tensor_stub.c
- README.md
- build.yml
- head-custom.html
- mathjax.html
- default.html
- style.scss
- search.js
- torchlean-logo.png
- attention-masks.png
- batch-invariance.png
- float-autograd-boundaries.png
- geometry3d-projection-bugzoo-contact-sheet.png
- geometry3d-wilddet3d-bbox-diagnostic.png
- geometry3d-wilddet3d-contact-sheet.png
- kv-cache-rope.png
- normalization-state.png
- tokenizer-boundaries.png
- autograd-basics-new.png
- autograd-basics.png
- bug-zoo-new.png
- bug-zoo.png
- bug-zoo.svg
- diffusion-new.png
- diffusion-real-images.png
- float32-ieee-new.png
- float32-ieee.png
- geometry3d-vision-certificates.png
- geometry3d-vision-new.png
- gpt-text-new.png
- gpt2-text.png
- graph-ir-bounds-new.png
- ir-bounds.png
- mamba-text.png
- mlp-cnn-training.png
- pytorch-roundtrip-new.png
- pytorch-roundtrip.png
- reinforcement-learning-new.png
- reinforcement-learning.png
- scientific-ml-new.png
- supervised-training-new.png
- verification-bounds-new.png
- verification-bounds.png
- cnn_cuda_300_xent_adam.png
- diffusion_cuda_50.png
- fno_cuda_50.png
- gpt2_cuda_300_w32.png
- lstm_regression_cuda_100.png
- mamba_cuda_200.png
- mlp_cuda_1000_adam.png
- resnet_cuda_200.png
- vit_cuda_100.png
- diffusion_imagenette64_real_vs_generated_plot.png
- torchlean-layout.png
- torchlean_logo.svg
- index.md
- index.md
- index.md
- index.md
- index.md
- index.md
- index.md
- index.md
- index.md
- dependency-audit.json
- index.md
- index.html
- index.md
- index.md
- index.md
- index.md
- index.md
- 404.html
- _config.yml
- _config_dev.yml
- Gemfile
- Gemfile.lock
- index.md
- manual.md
- README.md
- search-index.json
- Training.lean
- Dataset.lean
- Loaders.lean
- README.md
- Sources.lean
- Synthetic.lean
- TensorDataset.lean
- Text.lean
- Training.lean
- CausalTransformer.lean
- Cnn.lean
- Diffusion.lean
- FNO.lean
- Generative.lean
- KAN.lean
- Mamba.lean
- PPO.lean
- Recurrent.lean
- ResNet.lean
- SelfSupervised.lean
- Transformer.lean
- Vit.lean
- Command.lean
- Execution.lean
- Blocks.lean
- Builders.lean
- Execution.lean
- Heads.lean
- Leading.lean
- Summary.lean
- Transformer.lean
- VisionLayers.lean
- Cli.lean
- Definitions.lean
- Runtime.lean
- BlockMask.lean
- Bpe.lean
- Generation.lean
- Options.lean
- Tokenizer.lean
- Unicode.lean
- Control.lean
- Core.lean
- Loops.lean
- Stepper.lean
- Custom.lean
- OneHotCrossEntropy.lean
- Regression.lean
- Streams.lean
- Constructor.lean
- Core.lean
- FixedSample.lean
- Manual.lean
- Predict.lean
- Reporting.lean
- Results.lean
- Run.lean
- Scheduler.lean
- Summary.lean
- Train.lean
- Adapters.lean
- Autograd.lean
- Checkpoint.lean
- CLI.lean
- Data.lean
- Init.lean
- Json.lean
- Loss.lean
- Macros.lean
- Models.lean
- Module.lean
- Neural.lean
- Optim.lean
- Rand.lean
- README.md
- RL.lean
- Runtime.lean
- Scalar.lean
- Seeded.lean
- SelfSupervised.lean
- Tensor.lean
- TensorPack.lean
- Text.lean
- Trainer.lean
- Verification.lean
- Accepted.lean
- Attention.lean
- Audit.lean
- Availability.lean
- Capsule.lean
- Gate.lean
- Grouping.lean
- IR.lean
- LibTorch.lean
- NativeCUDA.lean
- Planner.lean
- Profile.lean
- Recheck.lean
- Reference.lean
- Registry.lean
- Report.lean
- Target.lean
- Types.lean
- All.lean
- Examples.lean
- Floats.lean
- Foundation.lean
- README.md
- Runtime.lean
- SlowProofs.lean
- Tests.lean
- Theory.lean
- Verification.lean
- ExternalProcess.lean
- Numeric.lean
- All.lean
- AttentionMask.lean
- AutogradDomain.lean
- BatchInvariance.lean
- CompilerBoundary.lean
- ConstantNormalizationSlice.lean
- FloatBoundary.lean
- Geometry3DProjection.lean
- IgnoredLabelLoss.lean
- KVCache.lean
- LayerNormDegenerateAxis.lean
- NormalizationState.lean
- README.md
- RoPEPosition.lean
- ShapeAndBroadcast.lean
- StableLoss.lean
- TokenizerBoundary.lean
- Cifar10Images.lean
- Csv.lean
- Npy.lean
- Bands.lean
- generate_small_data.py
- Loaders.lean
- plot_fno1d_burgers.py
- prepare_fno1d_burgers.py
- README.md
- RealPaths.lean
- SamplePaths.lean
- ArbIEEEExecCompare.lean
- EffectiveRounding.lean
- Float32Semantics.lean
- GraphNumericalCertificate.lean
- Tutorial.lean
- Basic.lean
- IRAxisOps.lean
- OneSemanticUniverse.lean
- README.md
- TorchIRPyTorch.lean
- Widgets.lean
- Cholesky.lean
- Common.lean
- QR.lean
- Transcendentals.lean
- cnn.json
- Export.lean
- Import.lean
- train_cnn.py
- Export.lean
- Import.lean
- mlp.json
- train_mlp.py
- Export.lean
- Import.lean
- train_transformer.py
- transformer_encoder.json
- Export.lean
- Import.lean
- README.md
- Roundtrip.lean
- TorchExportCheck.lean
- PyTorch.lean
- README.md
- RealData.lean
- Train.lean
- Autoencoder.lean
- Diffusion.lean
- Gan.lean
- Mae.lean
- README.md
- Vae.lean
- VqVae.lean
- Fno1dBurgers.lean
- README.md
- DQNReplay.lean
- PPOCartPole.lean
- PPOGridWorld.lean
- PPOPongRam.lean
- README.md
- CharGpt.lean
- Gpt2.lean
- Gpt2Saved.lean
- GptAdder.lean
- Lstm.lean
- Mamba.lean
- README.md
- Rnn.lean
- TextGpt2.lean
- Transformer.lean
- Kan.lean
- LstmRegression.lean
- Mlp.lean
- README.md
- Cnn.lean
- README.md
- ResNet.lean
- Vit.lean
- Common.lean
- Generative.lean
- Operators.lean
- README.md
- RL.lean
- Runner.lean
- RunnerMain.lean
- Sequence.lean
- Supervised.lean
- Vision.lean
- Command.lean
- Training.lean
- MuonCertificates.lean
- README.md
- AutogradBasics.lean
- Common.lean
- MinibatchMlpTrain.lean
- Proofs.lean
- pytorch_translator_mlp.py
- README.md
- SimpleCnnTrain.lean
- SimpleMlpTrain.lean
- StarterWorkflow.lean
- TensorBasics.lean
- Widgets.lean
- GymnasiumRolloutView.lean
- PPOCartPoleView.lean
- PPOGridWorldView.lean
- PPOPongRamView.lean
- README.md
- example_raw_leaf_dump.json
- README.md
- sample_abcrown_leaf_artifact_v0_1.json
- attention_softmax_cert.json
- cnn_cert.json
- gru_gate_cert.json
- mlp_cert.json
- README.md
- transformer_encoder_cert.json
- logistic_learned_cert.json
- logistic_lower_learned.json
- logistic_trivial_cert.json
- logistic_upper_learned.json
- one_mlp.json
- README.md
- sample_ode_cert.json
- sin_cert.json
- zero_mlp.json
- zero_siren.json
- pinn_cert.json
- README.md
- sample_dataset_1d.json
- sample_dataset_2d.json
- digits_linear_margin_cert.json
- digits_linear_weights.json
- digits_test.json
- piecewise_linear_cert.json
- README.md
- README.md
- README.md
- Robustness.lean
- Splines.lean
- TorchLean.lean
- VNNComp.lean
- DeepDives.lean
- Factorization.lean
- Models.lean
- ModelZoo.lean
- Optimization.lean
- Quickstart.lean
- README.md
- RL.lean
- Verification.lean
- Zoo.lean
- arb_oracle.py
- Oracle.lean
- README.md
- Arithmetic.lean
- Bracket.lean
- Operations.lean
- README.md
- Round.lean
- Core.lean
- Error.lean
- Notation.lean
- README.md
- Sterbenz.lean
- Compare.lean
- Core.lean
- DyadicRounding.lean
- NearestEven.lean
- Ops.lean
- RatBounds.lean
- RoundDyadic.lean
- RoundRat.lean
- Ulp.lean
- Arithmetic.lean
- Core.lean
- Effective.lean
- MinMax.lean
- Order.lean
- RationalRounding.lean
- Representation.lean
- Rounding.lean
- ERealTotal.lean
- Expressions.lean
- FP32.lean
- FP32Total.lean
- LeanFloat32.lean
- Division.lean
- Positive.lean
- SignedOps.lean
- MkBitsToDyadic.lean
- MkBitsToReal.lean
- Negation.lean
- Arithmetic.lean
- Compare.lean
- Core.lean
- Directed.lean
- Dyadic.lean
- Instances.lean
- Transcendentals.lean
- NatLemmas.lean
- RatScaling.lean
- RoundDyadicToIEEE32Bounds.lean
- RoundQuotEvenBounds.lean
- RoundShiftRightEven.lean
- SpecialRules.lean
- TranscendentalRules.lean
- TrigBounds.lean
- TrigRules.lean
- ERealSemantics.lean
- ErrorBounds.lean
- MinMaxERealSoundness.lean
- OpSandwich.lean
- RealSemantics.lean
- Bridge.lean
- DirectedRoundingSoundness.lean
- Exec32.lean
- Notation.lean
- README.md
- Reductions.lean
- Comparison.lean
- ERealCoercions.lean
- FP32.lean
- IEEEExec32.lean
- IEEEExec32AddSoundness.lean
- IEEEExec32ArbTrans.lean
- IEEEExec32DivSoundness.lean
- IEEEExec32MinMaxSoundness.lean
- IEEEExec32MulSoundness.lean
- IEEEExec32NoNaN.lean
- IEEEExec32Soundness.lean
- Quantized.lean
- README.md
- RealBounds.lean
- Rounders.lean
- Neighbors.lean
- README.md
- StandardUlp.lean
- Sterbenz.lean
- SterbenzFLT.lean
- Ulp.lean
- Addition.lean
- Bounds.lean
- Directed.lean
- DivisionSqrt.lean
- Exactness.lean
- Multiplication.lean
- README.md
- Relative.lean
- Digits.lean
- Formats.lean
- Generic.lean
- Magnitude.lean
- README.md
- Theorems.lean
- Away.lean
- Core.lean
- Double.lean
- Generic.lean
- Nearest.lean
- Odd.lean
- Order.lean
- Predicates.lean
- Properties.lean
- README.md
- Conversion.lean
- NF.lean
- NNOps.lean
- README.md
- Representable.lean
- FTZ.lean
- README.md
- Analysis.lean
- Core.lean
- Error.lean
- Format.lean
- Metadata.lean
- README.md
- Rounding.lean
- Scalar.lean
- Special.lean
- Arb.lean
- Calc.lean
- Float32.lean
- FP32.lean
- IEEEExec.lean
- Interval.lean
- NeuralFloat.lean
- Quantization.lean
- README.md
- Core.lean
- LinearAlgebra.lean
- Nonlinear.lean
- Normalization.lean
- Shape.lean
- Core.lean
- Term.lean
- Autoencoder.lean
- Cnn.lean
- Mlp.lean
- TransformerBlock.lean
- Cnn.lean
- Mlp.lean
- MlpDeterministicInit.lean
- MlpSpecEquivalence.lean
- ResidualLinear.lean
- TorchLean.lean
- Embedding.lean
- Vision.lean
- Core.lean
- DAG.lean
- Models.lean
- Primitives.lean
- README.md
- ToSequential.lean
- Check.lean
- Graph.lean
- HardMask.lean
- Infer.lean
- OpContracts.lean
- Payload.lean
- Pretty.lean
- README.md
- Semantics.lean
- AlphaBetaCROWN.lean
- AlphaCROWN.lean
- AlphaConfig.lean
- BoundOpsIEEE32Exec.lean
- FloatIntegration.lean
- FP32.lean
- IntervalLemmas.lean
- Activations.lean
- Linear.lean
- Node.lean
- Run.lean
- Structural.lean
- Affine.lean
- BackwardObjective.lean
- Base.lean
- CROWN.lean
- Derivatives.lean
- IBP.lean
- Backward.lean
- Core.lean
- Engine.lean
- Theorems.lean
- .gitkeep
- Core.lean
- ExecUtils.lean
- LossAnalysis.lean
- PipelineIIHybrid.lean
- PipelineIIIAllInLean.lean
- PipelineIPythonOnly.lean
- Run.lean
- Certificate.lean
- Verification.lean
- Mlp.lean
- Activations.lean
- Arithmetic.lean
- BatchNorm.lean
- Conv.lean
- Slice.lean
- Trigonometric.lean
- Alpha.lean
- AlphaBeta.lean
- Common.lean
- CertificateStep.lean
- IntervalLemmas.lean
- Main.lean
- NonlinearOps.lean
- Semantics.lean
- AlphaBetaReLUScalarSoundness.lean
- AlphaReLULowerBound.lean
- Distillation.lean
- GraphAlphaCrownTransferSoundness.lean
- GraphCertSoundness.lean
- GraphCrownCertSoundness.lean
- GraphIBPBasicTheorems.lean
- GraphRunibpEndToEnd.lean
- Overview.lean
- SoundnessProofs.lean
- Backward.lean
- LinearSignsplit.lean
- Ops.lean
- CertificateWorkflow.lean
- crown_verifier.py
- BoundOps.lean
- Core.lean
- Flatbox.lean
- Graph.lean
- Operators.lean
- README.md
- ForwardGaussian.lean
- Samplers.lean
- GAN.lean
- Objective.lean
- VAE.lean
- VQVAE.lean
- Diffusion.lean
- Latent.lean
- Core.lean
- Runtime.lean
- Spec.lean
- Runtime.lean
- Spec.lean
- Core.lean
- ExampleDataset.lean
- IEEE32Exec.lean
- Real.lean
- Core.lean
- Dynamics.lean
- RidgeRegression1D.lean
- DifferentialPrivacy.lean
- Robustness.lean
- Stability.lean
- Certificates.lean
- Core.lean
- NewtonSchulz.lean
- QR.lean
- FirstOrder.lean
- GDLinearConvergence.lean
- Muon.lean
- OptimizerLaws.lean
- README.md
- SmoothStrongConvexBridge.lean
- StronglyConvexGD.lean
- ConstantTarget.lean
- ExactImageTheorem.lean
- Semantics.lean
- IEEE32ExecCore.lean
- UniversalApproximation.lean
- UniversalApproximationFP32.lean
- UniversalApproximationIEEE32Exec.lean
- UniversalApproximationIEEE32ExecTwoLayerMlp.lean
- UniversalApproximationND.lean
- UniversalApproximationRate.lean
- FloatInterval.lean
- Universal.lean
- Basic.lean
- Convergence.lean
- Dynamics.lean
- Energy.lean
- Progress.lean
- ReLUMulApprox.lean
- CompactSet.lean
- ReLUMlpBridge.lean
- MambaCausality.lean
- Scan.lean
- LipschitzCertified.lean
- MlpRobustness.lean
- Robustness.lean
- Approximation.lean
- Hopfield.lean
- ReLU.lean
- StateSpace.lean
- Verification.lean
- JEPA.lean
- MAE.lean
- Masking.lean
- PredictiveView.lean
- VICReg.lean
- API.lean
- LearningTheory.lean
- Proofs.lean
- README.md
- SelfSupervised.lean
- Dropout.lean
- Fft.lean
- FftBridge.lean
- InductiveProperties.lean
- Lipschitz.lean
- Normalization.lean
- Softmax.lean
- RealCorrectness.lean
- SemiringCorrectness.lean
- Vectorization.lean
- Core.lean
- Elementwise.lean
- LogSoftmax.lean
- MlpMse.lean
- OpSpec.lean
- Params.lean
- Softmax.lean
- Accumulation.lean
- BackwardGraph.lean
- BackwardGraphData.lean
- Core.lean
- FDeriv.lean
- Invariants.lean
- Link.lean
- PackedTensor.lean
- Nodes.lean
- Soundness.lean
- FDeriv.lean
- Soundness.lean
- BCEWithLogits.lean
- CrossEntropy.lean
- KLDivergence.lean
- MSE.lean
- NLL.lean
- Arithmetic.lean
- Batched.lean
- Context.lean
- Elementwise.lean
- GraphComposition.lean
- Losses.lean
- Matrix.lean
- Piecewise.lean
- Reductions.lean
- Shape.lean
- Softmax.lean
- MaskedMultiHeadSelfAttention.lean
- MaskedScaledDotProduct.lean
- MultiHeadSelfAttention.lean
- ScaledDotProduct.lean
- Common.lean
- Input.lean
- Kernel.lean
- Main.lean
- BackwardDot.lean
- FDeriv.lean
- GatherRows.lean
- BatchNormChannelFirst.lean
- LayerNorm.lean
- ElmanCell.lean
- DecoderBlock.lean
- EncoderBlock.lean
- FeedForward.lean
- PostNorm.lean
- ResidualAttention.lean
- Idx.lean
- Nodes.lean
- StepAlgebra.lean
- Coverage.lean
- Notation.lean
- Overview.lean
- Activation.lean
- Linear.lean
- ShapeContracts.lean
- CausalMask.lean
- PermutationEquivariance.lean
- Weights.lean
- Attention.lean
- Mlp.lean
- DiffusionForward.lean
- DQN.lean
- GridWorld.lean
- CheckedRuntime.lean
- IEEE32Exec.lean
- Boundary.lean
- Core.lean
- Environment.lean
- FiniteStochasticMDP.lean
- FinsetSup.lean
- Gymnasium.lean
- MarkovMDP.lean
- MDP.lean
- Replay.lean
- Tactics.lean
- SpecApprox.lean
- Tolerance.lean
- CROWN.lean
- Layers.lean
- MLP.lean
- BackwardApprox.lean
- ForwardApprox.lean
- LinkAutogradAlgebra.lean
- NumericalCertificate.lean
- Backend.lean
- Linalg.lean
- Main.lean
- Primitive.lean
- Sparse.lean
- BiasKernel.lean
- Common.lean
- Input.lean
- RevNode.lean
- Binary.lean
- Core.lean
- SafeDivSigmoid.lean
- Softmax.lean
- SoftplusSafeLog.lean
- Unary.lean
- Elementwise.lean
- Nodes.lean
- Plumbing.lean
- Scalar.lean
- Sum.lean
- Attention.lean
- BackwardOps.lean
- Conv.lean
- ConvBackward.lean
- ConvForward.lean
- EndToEnd.lean
- FoldLemmas.lean
- Linalg.lean
- Normalization.lean
- Ops.lean
- Optimizers.lean
- ReductionOps.lean
- ShapeOps.lean
- SoftmaxAxis.lean
- RoundingApprox.lean
- BackwardScale.lean
- ForwardScale.lean
- ScaleApprox.lean
- Core.lean
- FP32.lean
- Graph.lean
- NF.lean
- Optimizer.lean
- Rounding.lean
- Scale.lean
- Algebra.lean
- BoundsNorms.lean
- Core.lean
- Factorizations.lean
- FactorizationsOrthonormal.lean
- FactorizationsReconstruction.lean
- Folds.lean
- LinearAlgebra.lean
- Algebra.lean
- Basic.lean
- List.lean
- MathFunctions.lean
- Enclosure.lean
- EnclosureBackends.lean
- ODE.lean
- Analysis.lean
- IR.lean
- Models.lean
- Probability.lean
- README.md
- RuntimeApprox.lean
- Tensor.lean
- Verification.lean
- ActivationsLoss.lean
- Backward.lean
- Base.lean
- ConvPool.lean
- Elementwise.lean
- Indexing.lean
- Linear.lean
- Neural.lean
- Shape.lean
- Attention.lean
- ConvPool.lean
- Core.lean
- Elementwise.lean
- Indexing.lean
- Linear.lean
- NormSoftmax.lean
- Shape.lean
- Buffer.lean
- Convert.lean
- ConvPool.lean
- DGemm.lean
- Float32Contract.lean
- Fno1dRfftFused.lean
- Kernels.lean
- KernelSpec.lean
- NativeSources.lean
- Ops.lean
- Shape.lean
- Tape.lean
- Trusted.lean
- Core.lean
- Cuda.lean
- FastKernels.lean
- TapeM.lean
- Activations.lean
- Constants.lean
- Elementwise.lean
- LinearAlgebra.lean
- Loss.lean
- Normalization.lean
- Permutation.lean
- Pooling.lean
- Random.lean
- Reductions.lean
- Structural.lean
- Unary.lean
- Common.lean
- Ops.lean
- SemanticEquivalence.lean
- SemanticEquivalenceCommon.lean
- SemanticEquivalenceOpCases.lean
- Primitives.lean
- API.lean
- Core.lean
- Correctness.lean
- Lowering.lean
- Convolution.lean
- Dispatch.lean
- Elementwise.lean
- Indexing.lean
- Layers.lean
- LinearAlgebra.lean
- Pooling.lean
- ShapeReduction.lean
- CudaAdam.lean
- Schema.lean
- Attention.lean
- Parameters.lean
- BackwardOptim.lean
- CheckpointIO.lean
- Functional.lean
- Ops.lean
- OptimizerCheckpoint.lean
- Session.lean
- Trainer.lean
- TypedGraph.lean
- Types.lean
- Autograd.lean
- ConvAttention.lean
- Core.lean
- GraphOps.lean
- Neural.lean
- ShapeIndex.lean
- Core.lean
- Initialization.lean
- ScalarTrainer.lean
- TypedGraphSession.lean
- Core.lean
- Einsum.lean
- ShapeOps.lean
- Activations.lean
- Attention.lean
- ConvPool.lean
- Core.lean
- Normalization.lean
- Recurrent.lean
- Seq.lean
- Autograd.lean
- Eager.lean
- Neural.lean
- Ops.lean
- ShapeIndex.lean
- Types.lean
- Autodiff.lean
- Dual.lean
- Fft.lean
- Fno.lean
- Fno1d.lean
- Functional.lean
- Loss.lean
- Metrics.lean
- Module.lean
- NN.lean
- Norm.lean
- Optim.lean
- Program.lean
- Random.lean
- Session.lean
- StateIO.lean
- Training.lean
- Csv.lean
- Npy.lean
- Parsing.lean
- Core.lean
- Dataset.lean
- Eval.lean
- IoLoader.lean
- Logging.lean
- Optim.lean
- Overview.lean
- TapeM.lean
- TensorLoader.lean
- Trainer.lean
- Convolution.lean
- Core.lean
- Elementwise.lean
- Neural.lean
- Pooling.lean
- ShapeIndex.lean
- Core.lean
- GraphM.lean
- Engine.lean
- IRExec.lean
- LeadingAxis.lean
- Overview.lean
- Torch.lean
- TorchLean.lean
- Train.lean
- TypedGraph.lean
- Julia.lean
- Core.lean
- Native.lean
- PyTorch.lean
- GradientUtils.lean
- Optimizers.lean
- README.md
- Schedulers.lean
- Core.lean
- IRPyTorch.lean
- ONNX.lean
- StateDict.lean
- TorchExport.lean
- Core.lean
- CrownParamstore.lean
- TorchExport.lean
- Export.lean
- Import.lean
- README.md
- Bandits.lean
- DQN.lean
- PolicyGradient.lean
- Tabular.lean
- ValueLearning.lean
- Path.lean
- Policy.lean
- Position.lean
- DefaultPaths.lean
- GridWorld.lean
- Core.lean
- Json.lean
- Client.lean
- Session.lean
- Advantage.lean
- Intervals.lean
- PPO.lean
- Returns.lean
- Types.lean
- Float32.lean
- Autograd.lean
- Collect.lean
- Rollout.lean
- Algorithms.lean
- Boundary.lean
- Core.lean
- Eval.lean
- Gymnasium.lean
- Numerics.lean
- PPO.lean
- Replay.lean
- Session.lean
- Log.lean
- Context.lean
- External.lean
- Optim.lean
- PyTorch.lean
- README.md
- RL.lean
- AutogradSpec.lean
- Ops.lean
- README.md
- API.lean
- Constructors.lean
- Core.lean
- Factorizations.lean
- Linalg.lean
- Numerics.lean
- Packed.lean
- Vec.lean
- Broadcasting.lean
- ConcatSlice.lean
- LinearAlgebra.lean
- Reductions.lean
- ShapeChange.lean
- Complex.lean
- Context.lean
- FloatInstances.lean
- README.md
- Scalar.lean
- Sequence.lean
- Shape.lean
- Tensor.lean
- TensorArray.lean
- TensorBridge.lean
- TensorGrad.lean
- TensorOps.lean
- TensorReductionShape.lean
- README.md
- StateSpace.lean
- System.lean
- Core.lean
- ForwardProcess.lean
- Loss.lean
- PFODE.lean
- ReverseDDIM.lean
- ReverseDDPM.lean
- Schedule.lean
- Diffusion.lean
- Latent.lean
- Padding.lean
- BatchNorm.lean
- Core.lean
- ND.lean
- PaddedTwoD.lean
- TwoD.lean
- Activation.lean
- Attention.lean
- Conv.lean
- Dropout.lean
- Embedding.lean
- FlashAttention.lean
- Gnn.lean
- Gru.lean
- Linear.lean
- Loss.lean
- Lstm.lean
- Normalization.lean
- Pooling.lean
- PositionalEncoding.lean
- README.md
- Rnn.lean
- SelectiveScan.lean
- Autoencoder.lean
- Cnn.lean
- Gan.lean
- Gmm.lean
- Gnn.lean
- GradientBoostedTrees.lean
- Hmm.lean
- Hopfield.lean
- Knn.lean
- LinearRegression.lean
- LogisticRegression.lean
- Mamba.lean
- Mlp.lean
- NaiveBayes.lean
- Pca.lean
- RandomForest.lean
- README.md
- S4.lean
- Seq2seq.lean
- Svm.lean
- Transformer.lean
- Unet.lean
- Vae.lean
- Vit.lean
- VqVae.lean
- Activation.lean
- Attention.lean
- Autoencoder.lean
- Conv.lean
- Core.lean
- DecisionTree.lean
- Dropout.lean
- Embedding.lean
- Flatten.lean
- Gnn.lean
- GradientBoostedTrees.lean
- GruModels.lean
- Hmm.lean
- Linear.lean
- LinearRegression.lean
- LogisticRegression.lean
- LstmModels.lean
- Normalization.lean
- Pca.lean
- Pooling.lean
- PositionalEncoding.lean
- README.md
- Rnn.lean
- RnnModels.lean
- Seq2seq.lean
- Svm.lean
- GridWorld.lean
- Core.lean
- Environment.lean
- FiniteStochasticMDP.lean
- MarkovMDP.lean
- MDP.lean
- README.md
- Autograd.lean
- Core.lean
- Dynamics.lean
- Generative.lean
- Layers.lean
- Models.lean
- Module.lean
- Quantization.lean
- README.md
- RL.lean
- API.lean
- README.md
- BlockMask.lean
- GradientAccumulation.lean
- Profile.lean
- CROWNOperators.lean
- Attention.lean
- BatchNorm.lean
- ConvPool.lean
- ConvTranspose.lean
- DeterministicReductions.lean
- Elementwise.lean
- Fft.lean
- GatherScatter.lean
- LayerNorm.lean
- LibTorchSDPA.lean
- LinearMseConcatSliceGather.lean
- MatmulBmm.lean
- PositionalEncoding.lean
- SelectiveScan.lean
- Softmax.lean
- Stress.lean
- Suite.lean
- Utils.lean
- ViewsBroadcastReduce.lean
- AllAutogradTests.lean
- CertificatePreconditions.lean
- IRBatchNorm.lean
- ONNXBridge.lean
- PINNDerivResidual.lean
- PyTorchRoundtripParity.lean
- RLCheck.lean
- StandaloneImport.lean
- Suite.lean
- TorchLeanIndexShapeCheck.lean
- TorchLeanIRExecEquivCheck.lean
- TorchLeanOpsCheck.lean
- TorchLeanSpecMlpEquivCheck.lean
- Utils.lean
- AutogradEngineTest.lean
- ElementwiseDivTest.lean
- Suite.lean
- README.md
- Suite.lean
- AbCrownLeafCert.lean
- CROWNNodeCert.lean
- CROWNNodeCertAlphaBeta.lean
- IBPCert.lean
- IBPNodeCert.lean
- NodeReplay.lean
- Box3D.lean
- check_box3d_camera_cert.json
- CLI.lean
- Attention.lean
- Cnn.lean
- ExampleInputs.lean
- Gru.lean
- Mlp.lean
- TransformerEncoder.lean
- Ast.lean
- Parse.lean
- Verify.lean
- Load.lean
- ParamStore.lean
- Architecture.lean
- Certificate.lean
- CLI.lean
- Core.lean
- Dataset.lean
- DatasetCheck.lean
- PdeAst.lean
- PdeParse.lean
- PyTorch.lean
- ResidualAffine.lean
- Digits.lean
- MarginCert.lean
- MarginCertCLI.lean
- TopLabel.lean
- TorchLean.lean
- PiecewiseLinearCLI.lean
- PiecewisePolyCert.lean
- API.lean
- Builder.lean
- BatchNorm.lean
- Concat.lean
- Core.lean
- Denote.lean
- Elementwise.lean
- LayerNorm.lean
- LinearAlgebra.lean
- LoweringPayload.lean
- Main.lean
- MiscOps.lean
- NodeShape.lean
- PayloadBridge.lean
- PayloadOps.lean
- Permutation.lean
- Pooling.lean
- Reductions.lean
- Return.lean
- ShapeOps.lean
- Softmax.lean
- Transpose.lean
- Eval.lean
- WellFormed.lean
- Correctness.lean
- Lowering.lean
- Syntax.lean
- Correctness.lean
- CrownOpsWorkflow.lean
- ExecutableLowering.lean
- IBPWorkflow.lean
- Lowering.lean
- MlpTrainVerifyWorkflow.lean
- Proved.lean
- SpecEval.lean
- TransformerIBPWorkflow.lean
- Array.lean
- FloatApprox.lean
- Json.lean
- Tensor.lean
- TextCursor.lean
- MnistFC.lean
- Spec.lean
- Cert.lean
- CLI.lean
- Geometry3D.lean
- LiRPA.lean
- Main.lean
- ODE.lean
- PINN.lean
- README.md
- Robustness.lean
- Splines.lean
- VNNComp.lean
- Docs.lean
- Tensor.lean
- UI.lean
- PyTorchTranslator.lean
- ExecutionTrace.lean
- Graph.lean
- Rewrite.lean
- ShapeInference.lean
- Gpt2.lean
- Float32.lean
- Boundary.lean
- GridWorld.lean
- PPO.lean
- Autograd.lean
- Context.lean
- Training.lean
- CROWN.lean
- README.md
- API.lean
- Backend.lean
- Docs.lean
- Floats.lean
- GraphSpec.lean
- IR.lean
- MLTheory.lean
- Proofs.lean
- Runtime.lean
- Spec.lean
- Tensor.lean
- Verification.lean
- Widgets.lean
- check.sh
- cuda_profile_tests.sh
- cuda_sanitize_tests.sh
- dependency_audit.py
- example_regression.sh
- repo_lint.py
- TorchLeanLint.lean
- download_example_data.py
- download_wikitext.py
- plot_trainlog.py
- torchlean_data_convert.py
- build_site.sh
- check_site_links.py
- polish_docgen.py
- polish_verso_guide.py
- export_gymnasium_rollout.py
- gymnasium_server.py
- train_ppo_cartpole_sb3.py
- resolve_libtorch.sh
- export_leaf_artifact.py
- README.md
- export_hf_depth_box3d_cert.py
- export_omni3d_box3d_cert.py
- export_wilddet3d_box3d_cert.py
- plot_box3d_bbox_diagnostic.py
- README.md
- realworld_manifest.json
- render_box3d_cert_overlay.py
- requirements-realworld.txt
- requirements-wilddet3d.txt
- safe_image_io.py
- test_bad_box3d_certs.py
- cert_runner.py
- common.py
- export_attention_cert.py
- export_cnn_cert.py
- export_crown_cert.py
- export_gru_cert.py
- export_mlp_cert.py
- export_pinn_cert.py
- export_pinn_weights.py
- import_burgers_shock_mat.py
- pinn_common.py
- safe_expr.py
- train_pinn_1d.py
- train_pinn_2d.py
- export_margin_cert.py
- train_digits_linear.py
- fit_piecewise_linear.jl
- cegis_van_stage2_python_baseline.py
- export_van_stage1_bits.py
- README.md
- regenerate_assets.py
- README.md
- .gitattributes
- .gitignore
- .gitpod.yml
- AGENTS.md
- AI_USAGE.md
- CITATION.cff
- CONTRIBUTING.md
- formalization.yaml
- lake-manifest.json
- lakefile.lean
- lean-toolchain
- LICENSE
- NN.lean
- README.md
- THIRD_PARTY_NOTICES.md
- TRUST_BOUNDARIES.md
// repository documentation
Was this content helpful?
(0 ratings)