[sympy] GSoC 2025: Seeking Feedback on Assumptions System Research & GSoC Project Choice

410 views
Skip to first unread message

Krishnav Bajoria

unread,
Feb 23, 2025, 2:12:48 PMFeb 23
to sympy

Hi SymPy Community,

I’m Krishnav Bajoria, a third-year student at IIT BHU,Varanasi in the department of Mathematics and Computing(GitHub handle - krishnavbajoria02).I am proficient in Python and have had a fairly strong mathematical background which was also the reason that led me to start contributing in SymPy. In terms of my contributions to SymPy, I have had three PRs merged—two related to assumptions and one in codegen/utilities.lambdify —and a few more under review.(Link to the PRs: https://github.com/sympy/sympy/pull/27511,https://github.com/sympy/sympy/pull/27512,https://github.com/sympy/sympy/pull/27552)

As I was exploring potential GSoC projects, I became particularly interested in two from the ideas page:

  1. Improvements to the Assumptions System
  2. The Risch Integration Algorithm

Since I’ve already worked a bit on assumptions, I’ve been delving deeper into the discussions and implementation details to understand its current state. I wanted to share what I’ve gathered so far and get feedback on whether I’m on the right track, or if there are other key areas I should focus on.

Assumptions System: What I’ve Studied So Far
  • Old vs. New Assumptions System:
    • The transition from the old rule-based system,which attached inferences directly to the objects as attributes, to the new predicate-based system,which separates inferences from objects and evaluates them dynamically, was meant to enhance flexibility. However, there are still inconsistencies where the new system does not propagate certain facts correctly.
  • Key Issues and Challenges:
    • Some assumptions are incorrectly inferred or not inferred at all due to missing rules.
    • Symbolic variables (e.g., x.is_real) sometimes fail to evaluate correctly when additional constraints are introduced.
    • Cases where the assumptions system contradicts itself in different parts of SymPy.
    • Performance concerns—some assumption queries take longer than expected due to inference chains.
  • Areas I’ve Been Exploring for Improvements:
    • Understanding handlers in the new system and whether they need restructuring.
    • Reviewing past discussions on improving assumptions and identifying still-relevant open issues.
    • Exploring ways to improve inference accuracy, especially in edge cases.
    • Considering whether any aspects of the old systemcould be reintroduced to address current limitations.

I’d appreciate to hear from the community—does this list cover the main areas that need attention? Are there any other fundamental issues I should be looking at?

Considering Risch Integration

Apart from assumptions, I’ve also started reading about the Risch integration algorithm. I haven’t explored it as deeply yet, but I find it intriguing and would like to get insights on its feasibility as a GSoC project.

At this stage, I’m just considering both projects for discussion and plan to finalize my choice based on the feedback and guidance from the community.

Thank you for your time and consideration. I look forward to your response!

Best Regards,
Krishnav Bajoria.

Krishnav Bajoria

unread,
Feb 23, 2025, 2:12:48 PMFeb 23
to sympy

Hi SymPy Community,

I’m Krishnav Bajoria, a third-year student at IIT BHU,Varanasi studying Mathematics and Computing.I am proficient in Python and have had a fairly strong mathematical background which was also the reason that led me to start contributing in SymPy. In terms of my contributions to SymPy, I have had three PRs merged—two related to assumptions and one in codegen/utilities.lambdify—and a few more under review.

As I was exploring potential GSoC projects, I became particularly interested in two from the ideas page:

  1. Improvements to the Assumptions System
  2. The Risch Integration Algorithm

Since I’ve already worked a bit on assumptions, I’ve been delving deeper into the discussions and implementation details to understand its current state. I wanted to share what I’ve gathered so far and get feedback on whether I’m on the right track, or if there are other key areas I should focus on.

Assumptions System: What I’ve Studied So Far

  • Old vs. New Assumptions System:
    • The transition from the old rule-based system,which attached inferences directly to the objects as attributes, to the new predicate-based system,which separates inferences from objects and evaluates them dynamically, was meant to enhance flexibility. However, there are still inconsistencies where the new system does not propagate certain facts correctly.
  • Key Issues and Challenges:
    • Some assumptions are incorrectly inferred or not inferred at all due to missing rules.
    • Symbolic variables (e.g., x.is_real) sometimes fail to evaluate correctly when additional constraints are introduced.
    • Cases where the assumptions system contradicts itself in different parts of SymPy.
    • Performance concerns—some assumption queries take longer than expected due to inference chains.
  • Areas I’ve Been Exploring for Improvements:
    • Understanding handlers in the new system and whether they need restructuring.
    • Reviewing past discussions on improving assumptions and identifying still-relevant open issues.
    • Exploring ways to improve inference accuracy, especially in edge cases.
    • Considering whether any aspects of the old system could be reintroduced to address current limitations.

Krishnav Bajoria

unread,
Feb 26, 2025, 10:45:35 PMFeb 26
to [email protected]
Hello everyone,
I wanted to follow up on my previous email regarding potential GSoC projects, particularly my exploration of improvements to the Assumptions system and the Risch Integration Algorithm.
I understand that everyone has busy schedules, but I would really appreciate any feedback on the key areas I outlined in my previous email- especially regarding the assumptions system and whether I’m on the right track in my analysis.Are there any specific issues or directions that you think I should focus on ?
Additionally, if there are any prior discussions or references that might help deepen my understanding, I’d be grateful if you could point me toward them.
Looking forward to any insights or guidance from the community!
Best Regards,
Krishnav Bajoria.

--
You received this message because you are subscribed to the Google Groups "sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [email protected].
To view this discussion visit https://groups.google.com/d/msgid/sympy/42483b67-c51d-442e-b245-61527ef09fdan%40googlegroups.com.

Aaron Meurer

unread,
Mar 3, 2025, 8:49:21 PMMar 3
to [email protected]
It looks like you've been making good progress on your pull requests
to the assumptions system. There is a lot of work that needs to be
done in the assumptions system, so the challenge for GSoC is finding a
small piece of that work that can be targeted for a suitable summer
project. There's a few important areas that the assumptions need to be
improved in. These areas are not completely independent, but it should
be possible to make a project that just focuses on one of them.

1. Improving the performance of the underlying system. An approach
here is to make better use of faster dependencies like Z3 as well as
SAT solvers. This also requires rewriting the existing code to use a
better approach that doesn't try to do too many things at once for
simple queries.

2. Reduce the parts of SymPy that make unnecessary use of the
assumptions. This is particularly the case in the core, where many
automatic operations use assumptions. Ideally no *automatic* operation
should use assumptions. By automatic, I mean the things that happen
when an expression object is constructed, without any further user
intervention. Here's a prototypical example:

In [1]: from sympy.functions.elementary._trigonometric_special import cos_257

In [2]: %time a = cos_257()
CPU times: user 8.52 s, sys: 314 ms, total: 8.83 s
Wall time: 8.82 s

It takes over 8 seconds just to *create* this expression, without
doing anything with it. And it isn't a particularly large expression,
at least for SymPy. (note that this function is cached so you'll need
to restart Python each time you want to time the function). See
https://github.com/sympy/sympy/pull/24566.

This is happening because the objects that are being created are
calling assumptions, which are doing relatively expensive numerical
calculations on the objects.

3. Implement new algorithms that improve the deductive capabilities of
the assumptions system. This is the sort of project that was done in
2023 https://github.com/sympy/sympy/wiki/GSoC-2023-Report-Tilo-Reneau%E2%80%90Cardoso:-Improving-Relational-Assumptions-in-SymPy%E2%80%99s-New-Assumptions.
There are a lot of potential directions here, but the thing that we
need the most is further improvements to assumptions on inequalities.

4. Rewrite the way assumptions handlers are written so that they use
something simpler and less error prone than the current 3-valued logic
_eval_is_* handlers. My idea is to use something based on pattern
matching. I haven't really fleshed this idea out much yet, so if
you're interested in it we'd need to work together to prototype what
it would look like.

As far as the Risch algorithm, there's also work that can be done
there, although if you're interested in that I would suggest reading
up on the Risch algorithm. A project there would be much more
mathematically involved. My suggestion for starting there would be
starting with Manual Bronstein's "Symbolic Integration Tutorial"
(there are other good resources too, including Bronstein's book) and
in particular, try to understand how the rational integration
algorithm works (currently implemented in SymPy in ratint.py). That is
the most basic part of the algorithm, and should at least give you an
idea of what the mathematics for Risch looks like.

Aaron Meurer

Krishnav Bajoria

unread,
Mar 3, 2025, 8:55:01 PMMar 3
to [email protected]
Hello Aaron,
Thank you so much for getting back to me as well as for the detailed response. I will go through this and further continue the discussion on the Google group regarding this.
Best Regards,
Krishnav Bajoria.

Tilo RC

unread,
Mar 8, 2025, 12:11:55 AMMar 8
to sympy
> 1. Improving the performance of the underlying system. An approach
here is to make better use of faster dependencies like Z3 as well as
SAT solvers. This also requires rewriting the existing code to use a
better approach that doesn't try to do too many things at once for
simple queries.

I don't think using faster dependencies will improve the speed. The process of passing the data to C++ is not very fast as the python bindings for Z3 are not very efficient which defeats the whole purpose. Maybe there is some other library that has more optimized python bindings though. In general, the SAT problems being solved are not very difficult so I don't think a more advanced algorithm would be all that helpful.

Currently, a single query to ask results in a lot of calls to satask due to all of the recursive calls made to the _eval_is_* handlers. So either a) reducing the number of calls to satask or b) making calls to satask, which are currently very expensive, more efficient would greatly speed up the assumptions. 

I have a few ideas for how to do both of these things:

a.1. Some form of caching can be implemented. Recursive calls to ask end up repeating the same calls to ask many times, so caching would avoid doing repeated work. It would also allow for some of the _eval_is_* handlers to be redesigned with the knowledge that caching is implemented in mind.

a.2. Maybe replace the _eval_is_* handlers completely with sathandlers rules. This would mean no more recursive calls at all so calls to ask are guaranteed to only call satask once. I'm not sure if this would always be possible for all of them though?

b.1. I came up with an SMT algorithm to replace the rules generated by facts.py which would greatly reduce the size of boolean satisfiability problems. I think I might want to implement this myself though if I have time. It may even be possible to come up with a more general algorithm that could replace the sathandlers and the _eval_is_* handlers entirely. 

b.2. The two SAT queries made by satask are very similar. If SymPy had an incremental sat solver, some repeated work could be avoided. See https://github.com/sympy/sympy/issues/27477. It might also be possible to check if the assumptions were inconsistent only once during a preprocessing step and not repeat this every single time a recursive call to ask is made. 

A third idea is to look into how Maple's assumption system works and take ideas from there. In most respects it's a lot better than SymPy's. There are several papers related to how it works:
- https://link.springer.com/chapter/10.1007/3-540-57272-4_27 
- https://dl.acm.org/doi/pdf/10.1145/120694.120749
There are also more papers that might be worth looking into in the list of papers that cite those two. It's also possible to actually look at the source code for Maple's assumption system, and even step through it using a debugger. Of course, Maple is proprietary software, so I'm not sure to what extent it would be legally okay to inspiration from it. You can get a free trial for Maple for 14 days. One reason not to go down this path is that Maple's assumption system works very differently than SymPy's in some ways, so it might be a lot of work to switch and not necessarily better. 


> 3. Implement new algorithms that improve the deductive capabilities of
the assumptions system. This is the sort of project that was done in
2023 https://github.com/sympy/sympy/wiki/GSoC-2023-Report-Tilo-Reneau%E2%80%90Cardoso:-Improving-Relational-Assumptions-in-SymPy%E2%80%99s-New-Assumptions.
There are a lot of potential directions here, but the thing that we
need the most is further improvements to assumptions on inequalities.

Currently, queries to ask that involve inequalities can only be solved if all of the variables involved are assumed to be real using the old assumptions. It would be nice to be able to handle complex queries in general — I think it would even be possible to handle queries that made assumptions about the imaginary component of variables. It would also be nice to be able to handle queries that involved variables that might not be finite, and queries with non-rational coefficients. I don't think implementing all of those changes would be too difficult, and this might be something I work on in the next few months. 

As part of a club at the college I go to, I've been trying to help some of the members contribute to SymPy and an ambitious goal for the club is to get them to implement the changes I described above. As there's only limited time in the semester and I'm not sure how much time they're be willing to invest in this, I'm not sure how much progress will get done. So far it's taken a full three weeks just to get their first pull requests opened two days ago. Hopefully progress will speed up. 


> 4. Rewrite the way assumptions handlers are written so that they use
something simpler and less error prone than the current 3-valued logic
_eval_is_* handlers. My idea is to use something based on pattern
matching. I haven't really fleshed this idea out much yet, so if
you're interested in it we'd need to work together to prototype what
it would look like.

It would be nice to be able to write them with a declarative paradigm. In other words, rather than using for loops and if statements and so on, it would be nice to be able to write rules in a form closer to actual mathematical logic. I think the sathandlers currently do a good job of this. For example, consider the sathandlers for sums:

### Add ##

@class_fact_registry.multiregister(Add)
def _(expr):
    return [allargs(x, Q.positive(x), expr) >> Q.positive(expr),
            allargs(x, Q.negative(x), expr) >> Q.negative(expr),
            allargs(x, Q.real(x), expr) >> Q.real(expr),
            allargs(x, Q.rational(x), expr) >> Q.rational(expr),
            allargs(x, Q.integer(x), expr) >> Q.integer(expr),
            exactlyonearg(x, ~Q.integer(x), expr) >> ~Q.integer(expr),
            ]

The single line "allargs(x, Q.positive(x), expr) >> Q.positive(expr)" (see these lines of code) is mostly equivalent to the following (except maybe the `_PositivePredicate_number` call):

@PositivePredicate.register(Add)
def _(expr, assumptions):
    if expr.is_number:
        return _PositivePredicate_number(expr, assumptions)

    r = ask(Q.real(expr), assumptions)
    if r is not True:
        return r

    nonneg = 0
    for arg in expr.args:
        if ask(Q.positive(arg), assumptions) is not True:
            if ask(Q.negative(arg), assumptions) is False:
                nonneg += 1
            else:
                break
    else:
        if nonneg < len(expr.args):
            return True

Actually, the handler above is more powerful because it understands that if a sum contains some positive and some zero terms, it will be postive while the sathandlers rule does not do this. But we could modify the sathandlers rule so that it was not just as powerful, but even more powerful:

Equivalent(Q.positive(expr), anyarg(x, Q.positive(x), expr) & allarg(x, Q.zero(x) | Q.positive(x), expr))

Assuming expr is of type Add, the line of logic above means: expr is positive if and only if at least one of its summands is positive and all of its summands are either zero or positive.

Anyway, the power of declarative programming is that you can specify what you want a program to do without worrying about the how. This means that you don't need nearly as many lines of code and the logic is a lot more human readable and closer to actual mathematical logic so it's easier to verify. 

Tilo Reneau-Cardoso

Aaron Meurer

unread,
Mar 8, 2025, 8:43:13 PMMar 8
to [email protected]
On Fri, Mar 7, 2025 at 2:12 PM Tilo RC <[email protected]> wrote:
>
> > 1. Improving the performance of the underlying system. An approach
> here is to make better use of faster dependencies like Z3 as well as
> SAT solvers. This also requires rewriting the existing code to use a
> better approach that doesn't try to do too many things at once for
> simple queries.
>
> I don't think using faster dependencies will improve the speed. The process of passing the data to C++ is not very fast as the python bindings for Z3 are not very efficient which defeats the whole purpose. Maybe there is some other library that has more optimized python bindings though. In general, the SAT problems being solved are not very difficult so I don't think a more advanced algorithm would be all that helpful.

Yes, the C-based solvers are really only going to help for the most
complex queries. What we really need though is to make common queries
faster. I think this basically boils down to two things:

- Make it simpler for the assumptions system to have "fast" queries
and "slow" queries and make the sorts of things that are called often
and need to be fast only use the fast queries.
- Avoid using assumptions at all in cases where they aren't needed.
You're right about all these things. But I just wanted to clarify that
for this point I was specifically talking about the old assumptions
handlers (the various _eval_is_* methods). These are the most
pervasive around SymPy and they are currently written with a 3-valued
logic that is difficult to do correctly. The problem with them is also
that they hard-code the computation of the assumptions, which limits
optimizations that can be done (currently only basic caching is
implemented).

Aaron Meurer
> To view this discussion visit https://groups.google.com/d/msgid/sympy/f093b5fb-53e9-4d2f-a769-b88d134760c0n%40googlegroups.com.

Krishnav Bajoria

unread,
Mar 16, 2025, 7:50:49 AMMar 16
to [email protected]
Hello again SymPy community,
First of all, I would like to thank Aaron and Tilo for their valuable comments and ideas. I have taken a note of them. For the past two weeks I have been studying through the entire assumptions system in SymPy and along with their ideas I have come up with some observations and my plan that I have for GSoC:
1) As pointed out earlier regarding the performance of assumptions I plan on making it faster and improving performance in the following ways:
- As suggested by Tilo, I would look to cache results in ways like currently @memoize decorator is used for in AssumptionKeys class. 
- By rewriting existing code for handlers by trying to take a two-fold approach as suggested by Aaron for fast queries and slow queries.
- I also think by improving abilities of refine, which currently has very less functionality added to it by improving that we can reduce number of calls when dealing with complex expressions.
2) By trying to improve the deductive capabilities and add functionalities related to quantifiers:
- I have been researching upon some new algorithms - as Tilo told that he will be implementing the SMT in his spare time so I wouldn't be looking into it then and instead would focus on elimination techniques like Fourier-Motzkin elimination, Quantifier elimination, Tarski's algorithm. 
- I also think we should be adding implementation and support for quantifiers for more general reasoning capability of SymPy. I think we could proceed in a way that is similar along the lines of functions like allargs, anyargs,etc which is written in a declarative programming paradigm and as was also suggested by Tilo we should add more general rules along these lines. I think quantifiers implementation along these lines would be a good idea.
Till now I have come up with mainly these observations and ideas and would appreciate any guidance or comments on these ideas if they are relevant and how much of an impact will this create to SymPy as a whole not just their assumptions module. Any additional algorithm or idea that could be added in assumptions system would be gladly welcome and helpful for me too. 
Best Regards,
Krishnav Bajoria.


Krishnav Bajoria

unread,
Mar 20, 2025, 2:45:55 PMMar 20
to [email protected]

Dear SymPy Community,

I hope you're doing well. I wanted to follow up regarding my GSoC proposal idea, as I haven’t received any further feedback. I appreciate the insights from Aaron and Tilo, and I’ve been working on refining my proposal based on the discussion.

Would it be possible for someone to review my updated proposal and provide any additional feedback? I want to ensure I’m on the right track and aligning with the community's expectations.

I’d really appreciate any guidance or suggestions on how I can further improve my proposal. Looking forward to your thoughts!

Best regards,
Krishnav Bajoria.

Aaron Meurer

unread,
Mar 20, 2025, 8:24:01 PMMar 20
to [email protected]
On Sat, Mar 15, 2025 at 10:50 PM Krishnav Bajoria <[email protected]> wrote:
Hello again SymPy community,
First of all, I would like to thank Aaron and Tilo for their valuable comments and ideas. I have taken a note of them. For the past two weeks I have been studying through the entire assumptions system in SymPy and along with their ideas I have come up with some observations and my plan that I have for GSoC:
1) As pointed out earlier regarding the performance of assumptions I plan on making it faster and improving performance in the following ways:
- As suggested by Tilo, I would look to cache results in ways like currently @memoize decorator is used for in AssumptionKeys class. 
- By rewriting existing code for handlers by trying to take a two-fold approach as suggested by Aaron for fast queries and slow queries.
- I also think by improving abilities of refine, which currently has very less functionality added to it by improving that we can reduce number of calls when dealing with complex expressions.
2) By trying to improve the deductive capabilities and add functionalities related to quantifiers:
- I have been researching upon some new algorithms - as Tilo told that he will be implementing the SMT in his spare time so I wouldn't be looking into it then and instead would focus on elimination techniques like Fourier-Motzkin elimination, Quantifier elimination, Tarski's algorithm. 
- I also think we should be adding implementation and support for quantifiers for more general reasoning capability of SymPy. I think we could proceed in a way that is similar along the lines of functions like allargs, anyargs,etc which is written in a declarative programming paradigm and as was also suggested by Tilo we should add more general rules along these lines. I think quantifiers implementation along these lines would be a good idea.

These are all good points of approach. My suggestion would be to focus more on just one or two of these. Otherwise, you will never end up being able to complete everything by the end of the summer, unless you only implement a half-baked solution for each. 

And for what it's worth, I think the "two-fold" idea is a lot harder than it sounds. It's something we've known we've needed to do for a long time, but it hasn't been really implemented. I don't want to discourage you if that's the project you want to do, but just be aware that it's going to require a good bit of prototyping to get a good design, and trial and error. Personally, I would suggest this project more for someone who is already fairly familing with the SymPy assumptions system(s) and the issues with them. Really, ideally, those of us who are already familiar with it should sit down and build a design for what this should look like so that it could actually be feasibly implemented in a GSoC project, but that hasn't happened yet. 

And anyways, it's generally useful to improve the capabilities of the "new" assumptions system without worrying about how to integrate it into the core. We will be able to design a much better integration into the core once we have a better idea of what the capabilities of the new system can be and how fast they can be. So a project just focused on implementing some algorithm is fine.

Aaron Meurer
 

Krishnav Bajoria

unread,
Mar 21, 2025, 8:08:12 AMMar 21
to [email protected]

Hello Aaron,
Thank you for your detailed feedback on my proposal ideas. I now realize that focusing on just 1-2 tasks from my initial list would be the best approach, and I’m currently working on finalizing my scope of work and drafting my proposal accordingly.
As I proceed, I had two questions:
1) I noticed that there isn’t a specific mentor yet listed for the assumptions project on the ideas page. Will a mentor be assigned, or should I continue engaging with the community for guidance? (Given your insights, I was wondering if you might also be involved in mentoring for this project.)
2) For proposal reviews, should I share my draft of the proposal in this public discussion, or is there a preferred way to receive feedback, such as direct communication with a mentor once assigned?
I’d appreciate any clarification so I can move forward in the best way possible.
Best Regards,
Krishnav Bajoria. 

Aaron Meurer

unread,
Mar 21, 2025, 8:55:45 PMMar 21
to [email protected]
On Thu, Mar 20, 2025 at 11:08 PM Krishnav Bajoria
<[email protected]> wrote:
>>
>> Hello Aaron,
>> Thank you for your detailed feedback on my proposal ideas. I now realize that focusing on just 1-2 tasks from my initial list would be the best approach, and I’m currently working on finalizing my scope of work and drafting my proposal accordingly.
>> As I proceed, I had two questions:
>> 1) I noticed that there isn’t a specific mentor yet listed for the assumptions project on the ideas page. Will a mentor be assigned, or should I continue engaging with the community for guidance? (Given your insights, I was wondering if you might also be involved in mentoring for this project.)

There's a number of people who could end up mentoring this project.
Unlike some projects, which are for specific parts of SymPy which only
one or two people would be able to mentor, there are a few of us who
could be a mentor on this one. Who would actually end up mentoring an
assumptions project depends on which other projects end up being
accepted and who is mentoring them.

>> 2) For proposal reviews, should I share my draft of the proposal in this public discussion, or is there a preferred way to receive feedback, such as direct communication with a mentor once assigned?

You can share it here, although if you prefer to only share it
privately you can do that as well.

Aaron Meurer

>> I’d appreciate any clarification so I can move forward in the best way possible.
>> Best Regards,
>> Krishnav Bajoria.
>
> --
> You received this message because you are subscribed to the Google Groups "sympy" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to [email protected].
> To view this discussion visit https://groups.google.com/d/msgid/sympy/CAF0TZutWFsdT03X-N2nuHCQ71EsBhuH1Cn6-4GyEpnAwckbhOA%40mail.gmail.com.

Krishnav Bajoria

unread,
Mar 30, 2025, 1:11:45 AMMar 30
to [email protected]

Dear SymPy Community,

I have completed the first draft of my GSOC 2025 proposal titled "Improving Relational Reasoning and Introducing Quantifier Support in SymPy's Assumptions Framework." You can find the proposal at this link.

I would greatly appreciate it if you could review the proposal and share any suggestions or feedback on how I can make it better. Your insights would be invaluable in refining the proposal further.

Thank you for your time and support!

Best regards,                                                                                                                                                                                                                    Krishnav Bajoria.


On Sun, Mar 23, 2025 at 1:49 AM Mailsuite Notification <[email protected]> wrote:

🔥 Hot conversation: [email protected] opened it many times in a short period or forwarded it. View all 459 opens | turn off hot conversations

Tilo RC

unread,
Mar 30, 2025, 1:54:41 AMMar 30
to [email protected]
Hi Krishnav,

I skimmed through your proposal. Could you make it more clear when you're paraphrasing something I wrote vs your own original thoughts? It would be good if you added footnotes for this sort of thing. Also, if you're paraphrasing stuff I wrote in particular issues, you should add links to those issues in the reference section. 

One more thing: Q.gt(x, 0) and Q.positive(x) are not supposed to be equivalent. Q.positive(x) implies that x is real whereas Q.gt(x, 0) implies x is extended real (it might not be finite).

Tilo Reneau-Cardoso

--
You received this message because you are subscribed to a topic in the Google Groups "sympy" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/sympy/XSJuvibPOro/unsubscribe.
To unsubscribe from this group and all its topics, send an email to [email protected].
To view this discussion visit https://groups.google.com/d/msgid/sympy/CAF0TZutDGaxUcgVK71ZzokOWN_87%3DwVzFA4F%2BaJXyNBhkpy3Sw%40mail.gmail.com.

Krishnav Bajoria

unread,
Mar 30, 2025, 2:05:24 AMMar 30
to [email protected]

Hi Tilo,

Thank you for your feedback and for pointing out these issues.

Regarding the paraphrasing and referencing, I understand my mistake. Moving forward, I'll be more clear when distinguishing between your original content and my own thoughts by adding footnotes. Additionally, when paraphrasing content from specific issues, I'll include links to those issues in the reference section for better traceability. I apologize for the lack of clarity in the previous version and will correct this in my next revision.

As for the distinction between Q.gt(x, 0) and Q.positive(x), I realize I misunderstood the difference. You're right—Q.positive(x) does indeed imply that x is real, whereas Q.gt(x, 0) allows for x to be extended real, which might include infinite values. I'll revise the proposal to accurately reflect this distinction.

Thanks again for your observation and guidance. I'll make sure the next version addresses these points properly.

Best regards,
Krishnav Bajoria.

On Sun, Mar 30, 2025 at 4:24 AM Tilo RC <[email protected]> wrote:
Hi Krishnav,

I skimmed through your proposal. Could you make it more clear when you're paraphrasing something I wrote vs your own original thoughts? It would be good if you added footnotes for this sort of thing. Also, if you're paraphrasing stuff I wrote in particular issues, you should add links to those issues in the reference section. 

One more thing: Q.gt(x, 0) and Q.positive(x) are not supposed to be equivalent. Q.positive(x) implies that x is real whereas Q.gt(x, 0) implies x is extended real (it might not be finite).

Tilo Reneau-Cardoso

On Sat, Mar 29, 2025 at 3:11 PM Krishnav Bajoria <[email protected]> wrote:

Dear SymPy Community,

I have completed the first draft of my GSOC 2025 proposal titled "Improving Relational Reasoning and Introducing Quantifier Support in SymPy's Assumptions Framework." You can find the proposal at this link.

I would greatly appreciate it if you could review the proposal and share any suggestions or feedback on how I can make it better. Your insights would be invaluable in refining the proposal further.

Thank you for your time and support!

Best regards,                                                                                                                                                                                                                    Krishnav Bajoria.


--
You received this message because you are subscribed to a topic in the Google Groups "sympy" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/sympy/XSJuvibPOro/unsubscribe.
To unsubscribe from this group and all its topics, send an email to [email protected].
To view this discussion visit https://groups.google.com/d/msgid/sympy/CAF0TZutDGaxUcgVK71ZzokOWN_87%3DwVzFA4F%2BaJXyNBhkpy3Sw%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [email protected].
To view this discussion visit https://groups.google.com/d/msgid/sympy/CAEgDm30-yGWbb-0cxdn48p%3DquWqi3ez%3DrRKLG7KNi7amajvzqg%40mail.gmail.com.

Tilo RC

unread,
Mar 31, 2025, 8:29:00 AMMar 31
to sympy
Hi Krishnav,

I recommend reading the following if you haven't already: https://github.com/sympy/sympy/wiki/Assumptions#the-aims-of-assumptions

Tilo Reneau-Cardoso

Krishnav Bajoria

unread,
Apr 1, 2025, 1:02:13 PMApr 1
to [email protected]

Dear SymPy Community,

I would like to inform you that I have taken into account Tilo’s comments regarding paraphrasing, adding footnotes, and properly referencing the sources of certain content in my GSoC 2025 proposal.

I have now uploaded the revised version of my proposal, titled:
"Improving Relational Reasoning and Introducing Quantifier Support in SymPy’s Assumptions Framework", to the SymPy Wiki. The link to my revised proposal for convenience can be found here.

Please feel free to review it and share any further feedback. I appreciate your time and guidance throughout this process.

Best regards,                                                                                                                                                                                                                  Krishnav Bajoria.


Aaron Meurer

unread,
Apr 1, 2025, 8:14:58 PMApr 1
to [email protected]
On Sun, Mar 30, 2025 at 11:29 PM Tilo RC <[email protected]> wrote:
Hi Krishnav,


Just be aware that this is a pretty old page. A lot of the stuff on it is still relevant, but not all of it represents the thinking that has happened since it was written. 

For instance, when people started writing the "new assumptions" (ask, Q, refine), the idea was that this would completely replace the old assumptions (Symbol('x', positive=True), x.is_positive). However, the thinking now is that this is a mistake, because the old assumption is syntactically very useful. They are different in that one system attaches assumptions to a Symbol and one system keeps them separate. The advantage of attaching assumptions to a symbol is that you don't have to keep passing assumptions to every function. The only other alternative is to have global assumptions (which you can currently do with assume()), but this creates global state, which is problematic. However, the advantage of keeping the assumptions separate is that you can assume things on entire expressions, not just symbols. The new assumptions system also has the advantage of being based on predicate logic, which uses symbolic unevaluated predicate expressions, whereas the old assumptions use 3-valued logic which doesn't support unevaluated expressions, and thus is more buggy and harder to do certain things with. Oscar and I talked a bit about these things (and others) in our 2022 SageDays talk https://www.youtube.com/watch?v=ujWoGQt7F5A (the talk starts at 1:46:30, and there is also some discussion at the end of the video). Slides are at https://docs.google.com/presentation/d/1SqV-Pcs_78z5oJItHafnystDr71AN1XBipP4FXEtjaA/edit?slide=id.p#slide=id.p

Aaron Meurer


Krishnav Bajoria

unread,
Apr 2, 2025, 7:46:03 PMApr 2
to [email protected]

Hi Tilo and Aaron,

Thank you both for your insights!

To Tilo, I appreciate you pointing me to the assumptions page—I wasn’t aware of some of the details, and it was really informative to read through.                                                                                                                                                                                                                      To Aaron, thanks for elaborating on the evolution of the assumptions system and its implications. Your explanation and the slides provided great clarity on the reasoning behind both approaches.                                                                                                                                                      I’ll reflect on what I’ve learned from this discussion and see how I can incorporate it into my GSoC project and proposal.

Best regards,
Krishnav Bajoria.


Tilo RC

unread,
Apr 3, 2025, 6:41:09 AMApr 3
to sympy
Krishnav, you might also want to take a quick look at this PR I'm working on: https://github.com/sympy/sympy/pull/27835

Tilo Reneau-Cardoso

Krishnav Bajoria

unread,
Apr 3, 2025, 11:10:38 AMApr 3
to [email protected]

Hello Tilo,

I've been analyzing that PR since you pushed it. Given the size of the code, it's taking some time to review it thoroughly, but I'll get back to you once I've gone through it completely.

Thanks again for pointing me to another valuable PR—it's been helpful for my understanding of SAT/SMT solvers.

Best Regards,                                                                                                                                                                                                                Krishnav Bajoria.


Tilo RC

unread,
Apr 3, 2025, 7:32:20 PMApr 3
to [email protected]
Don’t review it thoroughly. I don’t expect you to understand it. I just wanted you to know it exists.

--
You received this message because you are subscribed to a topic in the Google Groups "sympy" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/sympy/XSJuvibPOro/unsubscribe.
To unsubscribe from this group and all its topics, send an email to [email protected].

Krishnav Bajoria

unread,
Apr 3, 2025, 11:58:36 PMApr 3
to [email protected]
Hello everyone,
I have made some more changes to the timeline in my proposal. Please review it here and let me know what you think. If there is anything anyone would like me to change I would be happy to do so.
Also to Tilo, I understand that PR was more to deepen my understanding and have a look through/glance rather than a thorough review.
Best regards,
Krishnav Bajoria.

You received this message because you are subscribed to the Google Groups "sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [email protected].
To view this discussion visit https://groups.google.com/d/msgid/sympy/CAEgDm30cguwMTDYiUwzD1sBY4PZxGQzKGz%3DX%3DCEzsKMEj8QUgA%40mail.gmail.com.

Aaron Meurer

unread,
Apr 6, 2025, 9:06:18 AMApr 6
to [email protected]
I think you should go into more details with the quantifiers. Second order formulas can quickly get you into the realm of undecidable problems. Also some quantifier elimination algorithms are complex (for instance, CAD, which is one of the other GSoC idea projects, is a quantifier elimination algorithm). I would just start with getting the basic symbolic implemented, and maybe implement some simple deductions on them. The inability to symbolically represent quantifiers in SymPy's logic system has never been an issue, which is why they haven't been implemented yet. But it would be useful to have them. You should also look at other systems such as Sage, Z3, Maple, Mathematica, and other systems to see how they implement quantifiers and what sorts of operations they support.

Alternatively, if you want to deemphasize the quantifier part of your application and emphasize the algorithmic improvement parts instead, that would also be fine. The algorithmic improvements are more important than implementing quantifiers. Symbolic quantifiers would be nice, but as I've noted part of the reason they've never been implemented is that we haven't needed them. The main benefit they would provide to the assumptions would be the ability to represent certain types of facts in a more compact way. 

Aaron Meurer

To view this discussion visit https://groups.google.com/d/msgid/sympy/CAF0TZusUYieF4s-DJJNPGLnrvz2LrLhrEZnPR%2BpGo55JVKn2GQ%40mail.gmail.com.

Krishnav Bajoria

unread,
Apr 6, 2025, 5:15:22 PMApr 6
to [email protected]

Dear Aaron,

Firstly, thank you for reviewing my GSoC proposal and providing invaluable feedback. Based on your suggestions, I have revised my proposal to better align with SymPy's priorities and focus on algorithmic improvements.

Key Updates

  1. Quantifier Implementation:
    While I understand the importance of quantifiers in formal logic systems, I also recognize that their implementation can introduce complexity, especially with quantifier elimination algorithms (e.g., CAD). Given that symbolic quantifiers are not urgently needed for SymPy's assumptions system, I have reduced the scope of quantifier implementation in my timeline. Instead, I emphasize basic symbolic support inspired by Z3's pattern-based approach for universal (Q.forall) and existential (Q.exists) quantifiers.

  2. Algorithmic Improvements:
    Following your advice, I have placed greater emphasis on improving existing algorithms in the assumptions system. 

I have uploaded the updated proposal to the SymPy wiki page for your review:

Updated Proposal

I would be happy to incorporate further changes if needed and look forward to hearing your thoughts on this revised plan. Thank you once again for your guidance!

Best regards,

Krishnav Bajoria.


Reply all
Reply to author
Forward
0 new messages