Datasets:

RajasankarV
/

LeanCode-OpenAI-Math-Grouping

Error code:   DatasetGenerationError
Exception:    CastError
Message:      Couldn't cast
cluster_id: int64
cluster: list<item: int64>
  child 0, item: int64
confidence: double
data: list<item: string>
  child 0, item: string
doc_id: int64
domain_name: string
folder_name: string
file_name: string
to
{'doc_id': Value('int64'), 'data': List(Value('string')), 'folder_name': Value('string'), 'domain_name': Value('string'), 'file_name': Value('string')}
because column names don't match
Traceback:    Traceback (most recent call last):
                File "/usr/local/lib/python3.14/site-packages/datasets/builder.py", line 1827, in _prepare_split_single
                  for key, table in generator:
                                    ^^^^^^^^^
                File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 613, in wrapped
                  for item in generator(*args, **kwargs):
                              ~~~~~~~~~^^^^^^^^^^^^^^^^^
                File "/usr/local/lib/python3.14/site-packages/datasets/packaged_modules/json/json.py", line 343, in _generate_tables
                  self._cast_table(pa_table, json_field_paths=json_field_paths),
                  ~~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                File "/usr/local/lib/python3.14/site-packages/datasets/packaged_modules/json/json.py", line 132, in _cast_table
                  pa_table = table_cast(pa_table, self.info.features.arrow_schema)
                File "/usr/local/lib/python3.14/site-packages/datasets/table.py", line 2378, in table_cast
                  return cast_table_to_schema(table, schema)
                File "/usr/local/lib/python3.14/site-packages/datasets/table.py", line 2306, in cast_table_to_schema
                  raise CastError(
                  ...<3 lines>...
                  )
              datasets.table.CastError: Couldn't cast
              cluster_id: int64
              cluster: list<item: int64>
                child 0, item: int64
              confidence: double
              data: list<item: string>
                child 0, item: string
              doc_id: int64
              domain_name: string
              folder_name: string
              file_name: string
              to
              {'doc_id': Value('int64'), 'data': List(Value('string')), 'folder_name': Value('string'), 'domain_name': Value('string'), 'file_name': Value('string')}
              because column names don't match
              
              The above exception was the direct cause of the following exception:
              
              Traceback (most recent call last):
                File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 1369, in compute_config_parquet_and_info_response
                  parquet_operations, partial, estimated_dataset_info = stream_convert_to_parquet(
                                                                        ~~~~~~~~~~~~~~~~~~~~~~~~~^
                      builder, max_dataset_size_bytes=max_dataset_size_bytes
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                  )
                  ^
                File "/src/services/worker/src/worker/job_runners/config/parquet_and_info.py", line 948, in stream_convert_to_parquet
                  builder._prepare_split(split_generator=splits_generators[split], file_format="parquet")
                  ~~~~~~~~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                File "/usr/local/lib/python3.14/site-packages/datasets/builder.py", line 1694, in _prepare_split
                  for job_id, done, content in self._prepare_split_single(
                                               ~~~~~~~~~~~~~~~~~~~~~~~~~~^
                      gen_kwargs=gen_kwargs, job_id=job_id, **_prepare_split_args
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                  ):
                  ^
                File "/usr/local/lib/python3.14/site-packages/datasets/builder.py", line 1879, in _prepare_split_single
                  raise DatasetGenerationError("An error occurred while generating the dataset") from e
              datasets.exceptions.DatasetGenerationError: An error occurred while generating the dataset

Need help to make the dataset viewer work? Make sure to review how to configure the dataset viewer, and open a discussion for direct support.

doc_id int64	data list	folder_name string	domain_name string	file_name string
0	[ "import Mathlib.Algebra.MvPolynomial.CommRing", "import Mathlib.Basic.Complex.Basic", "import Mathlib.RingTheory.Ideal.Quotient.Operations", "namespace OAI", "namespace AbhyankarSathaye", "/-- In every dimension at least four, a polynomial can define affine space", "without being a coordinate of the amb...	math-main/lean/ComparatorChallenges/AbhyankarSathaye.lean	ComparatorChallenges	AbhyankarSathaye.lean
1	[ "import Mathlib", "namespace OAI", "noncomputable section", "open Set MeasureTheory", "open scoped BigOperators ContDiff ENNReal", "namespace AffineBernstein", "abbrev Space (n : N) := EuclideanSpace R (Fin n)", "def coordinateVector (n : N) (i : Fin n) : Space n :=", "EuclideanSpace.single i 1", ...	math-main/lean/ComparatorChallenges/AffineBernstein.lean	ComparatorChallenges	AffineBernstein.lean
2	[ "import Mathlib", "namespace OAI", "/-! Deterministic polynomial-time construction of strong thin trees. -/", "namespace StrongThinTree", "structure MultiGraph (n m : N) where", "left : Fin m - Fin n", "right : Fin m - Fin n", "loopless : [?] e, left e [?] right e", "namespace MultiGraph", "def cu...	math-main/lean/ComparatorChallenges/AlgorithmicThinTrees.lean	ComparatorChallenges	AlgorithmicThinTrees.lean
3	[ "import Mathlib", "namespace OAI", "universe u", "noncomputable section", "open scoped BigOperators ComplexOrder", "open Matrix Filter", "namespace GAD", "abbrev Basis (n : N) := Fin n - Fin 2", "abbrev QMatrix (n : N) := Matrix (Basis n) (Basis n) C", "/-- The spectral definition of -Tr(P log P),...	math-main/lean/ComparatorChallenges/AmplitudeDamping.lean	ComparatorChallenges	AmplitudeDamping.lean
4	[ "import Mathlib", "namespace OAI", "noncomputable section", "open scoped BigOperators ContDiff", "namespace ArnoldCounterexample", "abbrev CV := Fin 5 - C", "def quadricPolynomial (z : CV) : C := [?] j, z j ^ 2", "def normSquared (z : CV) : R := [?] j, Complex.normSq (z j)", "def IsUnitQuadric (z : ...	math-main/lean/ComparatorChallenges/ArnoldCounterexample.lean	ComparatorChallenges	ArnoldCounterexample.lean
5	[ "import Mathlib", "namespace OAI", "namespace ArtinCAT0", "universe uS uG uX", "abbrev Letters := Fin 116", "abbrev Label := WithTop N", "def blockLetter (b : Fin 3) (i : Fin 39) : Letters :=", "if h0 : i.val = 0 then <b.val, by omega> ", "else if h1 : i.val = 1 then <(b.val + 1) % 3, by omega> ", ...	math-main/lean/ComparatorChallenges/ArtinCAT0.lean	ComparatorChallenges	ArtinCAT0.lean
6	[ "import Mathlib", "namespace OAI", "/-! Parabolic intersections, parabolic closure, and non-clique Artin-group dynamics. -/", "namespace HarmonicArtin", "universe u", "variable {S : Type u}", "def alternating (s t : S) : N - FreeGroup S", "\| 0 => 1", "\| n + 1 => FreeGroup.of s * alternating t s n", ...	math-main/lean/ComparatorChallenges/ArtinParabolicIntersections.lean	ComparatorChallenges	ArtinParabolicIntersections.lean
7	[ "import Mathlib", "namespace OAI", "namespace AsymptoticallyMinimalLittlewood", "def littlewoodValue {N : N} (e : Fin N - R) (z : C) : C :=", "[?] k : Fin N, (e k : C) * z ^ (k : N)", "def IsRealSigning {N : N} (e : Fin N - R) : Prop :=", "[?] k, e k = -1 [?] e k = 1", "def MainStatement : Prop :=", ...	math-main/lean/ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean	ComparatorChallenges	AsymptoticallyMinimalLittlewood.lean
8	[ "import Mathlib", "namespace OAI", "noncomputable section", "open scoped BigOperators FourierTransform SchwartzMap", "open Complex Polynomial", "namespace AtomicTriangular", "abbrev Plane := EuclideanSpace R (Fin 2)", "def b : R := Real.sqrt 3 / 2", "def triangularPoint (jk : Z x Z) : Plane :=", "...	math-main/lean/ComparatorChallenges/AtomicGaussian.lean	ComparatorChallenges	AtomicGaussian.lean
9	[ "import Mathlib", "namespace OAI", "noncomputable section", "open CategoryTheory", "open scoped TensorProduct", "namespace ArExplicit.Statement", "universe u v", "abbrev K := FractionRing (MvPolynomial (Fin 3) (ZMod 2))", "def parameters (i : Fin 3) : K :=", "algebraMap (MvPolynomial (Fin 3) (ZMod...	math-main/lean/ComparatorChallenges/AuslanderReiten.lean	ComparatorChallenges	AuslanderReiten.lean
10	[ "import Mathlib", "namespace OAI", "namespace Hyperinvariant233", "open Filter", "open scoped Topology", "universe u", "variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace C H] [CompleteSpace H]", "def commutant (T : H -L[C] H) : Subalgebra C (H -L[C] H) :=", "Subalgebra.centralizer C ({...	math-main/lean/ComparatorChallenges/BackwardIntertwiners.lean	ComparatorChallenges	BackwardIntertwiners.lean
11	[ "import Mathlib", "namespace OAI", "open scoped BigOperators ContDiff", "namespace BoxTransport.Routing", "abbrev Space := Fin 3 - R", "abbrev RationalSpace := Fin 3 - Q", "abbrev SpaceTime := R x Space", "abbrev RationalSpaceTime := Q x RationalSpace", "abbrev Field := SpaceTime - Space", "abbrev...	math-main/lean/ComparatorChallenges/BalancedBoxRouting.lean	ComparatorChallenges	BalancedBoxRouting.lean
12	[ "import Mathlib", "namespace OAI", "namespace Balanced", "open scoped _root_.Balanced", "structure PartiteHypergraph (r n : N) where", "edges : Finset (Fin r - Fin n)", "namespace PartiteHypergraph", "variable {r n : N}", "abbrev Vertex (r n : N) := Fin r x Fin n", "def Covers (H : PartiteHypergra...	math-main/lean/ComparatorChallenges/BalancedRyser.lean	ComparatorChallenges	BalancedRyser.lean
13	[ "import Mathlib", "namespace OAI", "namespace BalancedTransport", "namespace Recorder", "inductive Direction where", "\| stay \| left \| right", "deriving DecidableEq", "instance : Fintype Direction :=", "<{.stay, .left, .right}, by intro d; cases d <;> simp> ", "structure Transition (Q G : Type*) wh...	math-main/lean/ComparatorChallenges/BalancedThreeStack.lean	ComparatorChallenges	BalancedThreeStack.lean
14	[ "import Mathlib", "namespace OAI", "namespace HigherDimensionalBallPacking", "open scoped ContDiff", "abbrev Phase (n : N) := Fin n - C", "noncomputable def capacity {n : N} (z : Phase n) : R :=", "Real.pi * [?] j, Complex.normSq (z j)", "def closedBall (n : N) (r : R) : Set (Phase n) := {z \| capacity...	math-main/lean/ComparatorChallenges/BallPacking.lean	ComparatorChallenges	BallPacking.lean
15	[ "import Mathlib", "namespace OAI", "namespace HigherDimensionalBallPacking", "open scoped ContDiff", "abbrev Phase (n : N) := Fin n - C", "noncomputable def capacity {n : N} (z : Phase n) : R :=", "Real.pi * [?] j, Complex.normSq (z j)", "def closedBall (n : N) (r : R) : Set (Phase n) := {z \| capacity...	math-main/lean/ComparatorChallenges/BallPackingNecessity.lean	ComparatorChallenges	BallPackingNecessity.lean
16	[ "import Mathlib", "namespace OAI", "namespace Barnette", "universe u", "/-- A topological plane drawing of a simple graph, with no crossings. -/", "structure PlaneEmbedding {V : Type u} (G : SimpleGraph V) where", "point : V - R x R", "point_injective : Function.Injective point", "arc : [?] (v w : V...	math-main/lean/ComparatorChallenges/BarnetteHamiltonian.lean	ComparatorChallenges	BarnetteHamiltonian.lean
17	[ "import Mathlib", "namespace OAI", "/-! Traces and augmentation rank on the idempotent presentation of algebraic K0. -/", "namespace BassTrace", "open scoped Classical", "noncomputable def classCoefficient {G : Type*} [Group G]", "(g : G) (a : MonoidAlgebra C G) : C := by", "classical", "exact a.coe...	math-main/lean/ComparatorChallenges/BassTorsionFree.lean	ComparatorChallenges	BassTorsionFree.lean
18	[ "import Mathlib.Algebra.Group.Conj", "import Mathlib.Algebra.MonoidAlgebra.Basic", "import Mathlib.Basic.Complex.Basic", "import Mathlib.GroupTheory.FreeAbelianGroup", "import Mathlib.GroupTheory.OrderOfElement", "import Mathlib.LinearAlgebra.Matrix.Trace", "import Mathlib.LinearAlgebra.Matrix.ToLin", ...	math-main/lean/ComparatorChallenges/BassTrace.lean	ComparatorChallenges	BassTrace.lean
19	[ "import Mathlib", "namespace OAI", "open MeasureTheory ProbabilityTheory", "open scoped ENNReal NNReal", "namespace Percolation", "universe u v", "variable {V : Type u} {E : Type v}", "abbrev BondGraph (V : Type u) (E : Type v) := E - Sym2 V", "def Adj (G : BondGraph V E) (x y : V) : Prop := [?] e, ...	math-main/lean/ComparatorChallenges/BenjaminiSchramm.lean	ComparatorChallenges	BenjaminiSchramm.lean
20	[ "import Mathlib", "namespace OAI", "noncomputable section", "open MeasureTheory Set Filter", "open scoped ENNReal Topology ContDiff", "namespace Bernoulli", "open scoped _root_.Bernoulli", "abbrev Space (d : N) := EuclideanSpace R (Fin d)", "/-- Compactly supported smooth real tests in the open set....	math-main/lean/ComparatorChallenges/BernoulliNonflatInSeven.lean	ComparatorChallenges	BernoulliNonflatInSeven.lean
21	[ "import Mathlib", "namespace OAI", "noncomputable section", "open Set MeasureTheory Manifold Bundle", "open scoped ContDiff Manifold ENNReal NNReal Topology", "namespace WeakMTWTransport", "abbrev Model (n : N) := EuclideanSpace R (Fin n)", "section MetricDefinitions", "variable {M : Type*} [MetricS...	math-main/lean/ComparatorChallenges/BiholderTransport.lean	ComparatorChallenges	BiholderTransport.lean
22	[ "import Mathlib", "namespace OAI", "noncomputable section", "namespace BinPackingGames.Foundations.Complexity", "def encodeWord (n : Nat) : List Bool := List.replicate n true ++ [false]", "end BinPackingGames.Foundations.Complexity", "namespace BinPackingGames.Foundations.Complexity.MachineFiniteAlphabe...	math-main/lean/ComparatorChallenges/BinPackingGap.lean	ComparatorChallenges	BinPackingGap.lean
23	[ "import Mathlib", "namespace OAI", "namespace TreeEdit", "universe u", "/-- A single unit-cost insertion, deletion, or substitution at any position. -/", "inductive EditStep {a : Type u} : List a - List a - Prop", "\| insert (p q : List a) (a : a) : EditStep (p ++ q) (p ++ a :: q)", "\| delete (p q : Li...	math-main/lean/ComparatorChallenges/BinaryEditLower.lean	ComparatorChallenges	BinaryEditLower.lean
24	[ "import Mathlib", "namespace OAI", "universe u_1 u_2", "namespace MatchingEntropy", "structure LooplessGraph (V : Type u_1) (E : Type u_2) where", "left : E - V", "right : E - V", "loopless : [?] e, left e [?] right e", "namespace LooplessGraph", "variable {V : Type u_1} {E : Type u_2} [Fintype V]...	math-main/lean/ComparatorChallenges/BinaryMatching.lean	ComparatorChallenges	BinaryMatching.lean
25	[ "import Mathlib", "namespace OAI", "noncomputable section", "open scoped BigOperators", "namespace BinaryCoordinateSweeps", "/-- The positions of a binary deck of dimension d. -/", "abbrev Slot (d : N) := Fin d - Bool", "/-- Independent switches on the edges parallel to one coordinate. -/", "def coo...	math-main/lean/ComparatorChallenges/BinarySweep.lean	ComparatorChallenges	BinarySweep.lean
26	[ "import Mathlib.Topology.Path", "import Mathlib.Topology.OpenPartialHomeomorph.Defs", "import Mathlib.Topology.Instances.Real.Lemmas", "import Mathlib.Data.Set.Finite.Basic", "import Mathlib.Data.Finset.Attr", "import Mathlib.Tactic.Common", "import Mathlib.Tactic.Finiteness.Attr", "import Mathlib.Tac...	math-main/lean/ComparatorChallenges/BipartiteCrossing.lean	ComparatorChallenges	BipartiteCrossing.lean
27	[ "import Mathlib", "namespace OAI", "noncomputable section", "namespace BogomolovPop", "def proEllKernel (ell : N) (G : Type*) [Group G] [TopologicalSpace G] : Subgroup G :=", " (H : OpenNormalSubgroup G) (_ : IsPGroup ell (G H.toSubgroup)), H.toSubgroup", "instance proEllKernel_normal (ell : N) (G : Ty...	math-main/lean/ComparatorChallenges/BogomolovPopInjectivity.lean	ComparatorChallenges	BogomolovPopInjectivity.lean
28	[ "import Mathlib", "namespace OAI", "/-!", "# Nonuniqueness for the periodic hard-sphere Boltzmann equation", "Theorem 1.1, with the full entropy-class admissibility of Definition 2.1 and", "strong initial L1 continuity with integrable collision gain and loss.", "-/", "noncomputable section", "open M...	math-main/lean/ComparatorChallenges/BoltzmannNonuniqueness.lean	ComparatorChallenges	BoltzmannNonuniqueness.lean
29	[ "import Mathlib", "namespace OAI", "namespace FiniteAlgebraicEnvelopes", "universe u", "abbrev Word (generatorCount : N) := List (Fin generatorCount x Bool)", "def evalWord {GroupType : Type u} [Group GroupType] {generatorCount : N}", "(generators : Fin generatorCount - GroupType) (word : Word generator...	math-main/lean/ComparatorChallenges/BooneHigman.lean	ComparatorChallenges	BooneHigman.lean
30	[ "import Mathlib", "namespace OAI", "namespace BorsukNine", "abbrev Vector4 := EuclideanSpace R (Fin 4)", "abbrev Matrix4 := EuclideanSpace R (Fin 4 x Fin 4)", "def projector (u : Vector4) : Matrix4 :=", "WithLp.toLp 2 (fun ij => u ij.1 * u ij.2)", "def projectorSet : Set Matrix4 :=", "projector '' {...	math-main/lean/ComparatorChallenges/BorsukNine.lean	ComparatorChallenges	BorsukNine.lean
31	[ "import Mathlib", "namespace OAI", "/-! Nondegenerate spectral calculus, the closed Tomita graph, and bounded recovery. -/", "universe u", "noncomputable section", "open Filter MeasureTheory Set", "open scoped Topology ComplexConjugate", "namespace BoundedRecovery", "variable {H : Type u} [NormedAdd...	math-main/lean/ComparatorChallenges/BoundedRecovery.lean	ComparatorChallenges	BoundedRecovery.lean
32	[ "import Mathlib", "namespace OAI", "noncomputable section", "universe u", "open Set", "open scoped ENNReal Classical", "namespace BoundedTreePotentials", "section TestNorms", "variable {I : Type}", "structure TestFamily (I : Type) where", "carrier : Set (I - R)", "zero_mem : (0 : I - R) [?] ...	math-main/lean/ComparatorChallenges/BoundedTreePotentials.lean	ComparatorChallenges	BoundedTreePotentials.lean
33	[ "import Mathlib", "namespace OAI", "noncomputable section", "namespace BoundedTreewidthL1", "universe u_1", "variable {V : Type u_1} (G : SimpleGraph V)", "/-- Sum of the given positive real edge lengths along a graph walk. -/", "def walkLength (l : G.edgeSet - R) : {u v : V} - G.Walk u v - R", "\| _...	math-main/lean/ComparatorChallenges/BoundedTreewidthL1.lean	ComparatorChallenges	BoundedTreewidthL1.lean
34	[ "import Mathlib", "namespace OAI", "noncomputable section", "open MeasureTheory", "open scoped BigOperators ENNReal", "namespace Problem358", "abbrev E (dimension : N) := EuclideanSpace R (Fin dimension)", "def uniformMeasure {dimension : N} (source : Set (E dimension)) : Measure (E dimension) :=", ...	math-main/lean/ComparatorChallenges/Brenier.lean	ComparatorChallenges	Brenier.lean
35	[ "import Mathlib", "namespace OAI", "noncomputable section", "open Set MeasureTheory Filter", "open scoped Topology", "namespace Brennan", "def disk : Set C := Metric.ball 0 1", "def UnivalentOn (f : C - C) (U : Set C) : Prop :=", "DifferentiableOn C f U [?] Set.InjOn f U", "def Schlicht (f : C - C...	math-main/lean/ComparatorChallenges/Brennan.lean	ComparatorChallenges	Brennan.lean
36	[ "import Mathlib", "namespace OAI", "noncomputable section", "open Set MeasureTheory Filter", "open scoped Topology ENNReal", "namespace Brennan", "def disk : Set C := Metric.ball 0 1", "def UnivalentOn (f : C - C) (U : Set C) : Prop :=", "DifferentiableOn C f U [?] Set.InjOn f U", "def Schlicht (f...	math-main/lean/ComparatorChallenges/BrennanSharp.lean	ComparatorChallenges	BrennanSharp.lean
37	[ "import Mathlib", "namespace OAI", "open scoped BigOperators Classical", "namespace BufferedIsing", "/-- A finite graph given by its edge list. Zero couplings can encode missing edges.", "Edges are indexed separately so parallel edges are counted separately. -/", "structure FiniteGraph (n m : N) where",...	math-main/lean/ComparatorChallenges/BufferedIsing.lean	ComparatorChallenges	BufferedIsing.lean
38	[ "import Mathlib", "namespace OAI", "namespace C0Absorption", "open scoped ZeroAtInfty", "abbrev C0 := C0(N, R)", "def BiLip {X Y : Type} [MetricSpace X] [MetricSpace Y] (f : X - Y) : Prop :=", "[?] c C : R, 0 < c [?] c <= C [?]", "[?] x y, c dist x y <= dist (f x) (f y) [?] dist (f x) (f y) <= C * ...	math-main/lean/ComparatorChallenges/C0Absorption.lean	ComparatorChallenges	C0Absorption.lean
39	[ "import Mathlib", "namespace OAI", "noncomputable section", "open CategoryTheory", "namespace Problem340", "abbrev ClockAmbient := EuclideanSpace R (Fin 2)", "abbrev SphereAmbient := EuclideanSpace R (Fin 3)", "abbrev StandardClock := Metric.sphere (0 : ClockAmbient) (1 : R)", "abbrev StandardSphere...	math-main/lean/ComparatorChallenges/C1EntropyCounterexample.lean	ComparatorChallenges	C1EntropyCounterexample.lean
40	[ "import Mathlib", "namespace OAI", "universe u", "noncomputable section", "namespace CHObstruction", "open Cardinal Ordinal Order", "structure RelModel (L : N - Type) where", "carrier : ZFSet.{u}", "rel : (n : N) - L n - (Fin n - carrier) - Prop", "namespace RelModel", "variable {L : N - Type}",...	math-main/lean/ComparatorChallenges/CHObstruction.lean	ComparatorChallenges	CHObstruction.lean

End of preview.

Dataset for OpenAI Lean Code grouping

Published Lean code is clustered via combinatorial hierarchical clustering

This is graph based combinatorial clustering not a statistical clustering in k-means clustering.

This combinatorial clustering finds context and meaning among the data.

Details

Total Files in the Github repo is 122141
Total Lean code lines 22358566
Total Lines taken for Clustering 5000000
Total Documents taken for Clustering 25391
Number of Code Line Clusters generated 248289
Number of File Clusters generated 3131
Total Lines in these clusters 3628607
Total Docs in these clusters 24738
% of lines which are clustered 72%
% of docs which are clustered 97%

How to understand the data

Finding similar contextual blocks allows the Lean code to be understood easily. Because the amount of generated code is so large that entire proofs can't be manually evaluated.
Finding similarity allows for easier code understanding because contextual comparison links both different part of code, files and domins easily.
Since this is LLM-generated Lean code for the mathematical proof, it will make tracing the reasoning or the method of LLM generation possible.
Full contextual clustering will be updated soon.

Method

The Lean code data is combined from all Lean code files in the GitHub repo.
The code data is fed to the Graph AI based combinatorial clustering method directly. No change.
The Graph AI compares the code lines via combinatorial clustering.
Resulting clusters of code lines.

Uses

Can be used understand how the Lean code is generated by LLMs.

Schema

All files are new line JSON files. It could be loaded as JSONL

data_file.json - Base Data file

doc_id - Unique ID for the file.
data - data from lean code files.
folder_name - folder name in which the Lean code file is located.
domain_name - domain name from the folder name location.
file_name - Lean code file name.

line_data.json - Contains lines used for Clustering

doc_id - Unique ID
line_id - Unique ID
line - Actual Lean Code line as it is.

rows_clusters.json

cluster_id - Unique ID denoting cluster.
cluster - List of line_id that forms a conceptual cluster.
confidence - Score of confidence showing how much these line_id are related.

docs_clusters.json

cluster_id - Unique ID denoting cluster
cluster - List of doc_id that forms a conceptual cluster.
confidence - Score of confidence showing how much these doc_id are related.

Downloads last month: 24

Total file size:

933 MB